Systematic Generation of Fast Elliptic Curve Cryptography Implementations

Widely used implementations of cryptographic primitives
employ number-theoretic optimizations specific to large
prime numbers used as moduli of arithmetic. These optimizations
have been applied manually by a handful of experts,
using informal rules of thumb. We present the first
automatic compiler that applies these optimizations, starting
from straightforward modular-arithmetic-based algorithms
and producing code around 5X faster than with off-the-shelf
arbitrary-precision integer libraries for C. Furthermore, our
compiler is implemented in the Coq proof assistant; it produces
not just C-level code but also proofs of functional
correctness. We evaluate the compiler on several key primitives
from elliptic curve cryptography

Source: https://people.csail.mit.edu/jgross/personal-website/papers/2018-fiat-crypto-pldi-draft.pdf

Advertisements

AES-VCM, An AES-GCM Construction Using An Integer-Based Universal Hash Function

We give a framework for construction and composition of universal
hash functions. Using this framework, we propose to swap out AES-GCM’s
F2128 -based universal hash function for one based on VMAC, which uses integer
arithmatic. For architectures having AES acceleration but where either
F2128 acceleration is absent or exists on the same execution unit as AES acceleration,
an integer-based variant of AES-GCM may offer a performance
advantage, while offering identical security.

Source: https://static.googleusercontent.com/media/research.google.com/en//pubs/archive/46483.pdf

A Vendor Agnostic Root of Trust for Measurement

We report the success of a project that Google performed as a proof-of-concept for increasing
confidence in first-instruction integrity across a variety of server and peripheral environments. We
begin by motivating the problem of first-instruction integrity and share the lessons learned from
our proof-of-concept implementation. Our goal in sharing this information is to increase industry
support and engagement for similar designs. Notable features include a vendor-agnostic capability
to interpose on the SPI peripheral bus (from which bootstrap firmware is loaded upon power-on in a
wide variety of devices today) without negatively impacting the efficacy of any existing vendor- or
device-specific integrity mechanisms, thereby providing additional defense-in-depth.

Source: https://static.googleusercontent.com/media/research.google.com/en//pubs/archive/46352.pdf

Implementing and Proving the TLS 1.3 Record Layer – Microsoft Research

The record layer is the main bridge between TLS applications and internal sub-protocols. Its core functionality is an elaborate form of authenticated encryption: streams of messages for each sub-protocol (handshake, alert, and application data) are fragmented, multiplexed, and encrypted with optional padding to hide their lengths. Conversely, the sub-protocols may provide fresh keys or signal stream termination to the record layer. Compared to prior versions, TLS 1.3 discards obsolete schemes in favor of a common construction for Authenticated Encryption with Associated Data (AEAD), instantiated with algorithms such as AES-GCM and ChaCha20-Poly1305. It differs from TLS 1.2 in its use of padding, associated data and nonces. It also encrypts the content-type used to multiplex between sub-protocols. New protocol features such as early application data (0-RTT and 0.5-RTT) and late handshake messages require additional keys and a more general model of stateful encryption. We build and verify a reference implementation of the TLS record layer and its cryptographic algorithms in F*, a dependently typed language where security and functional guarantees can be specified as pre-and post-conditions. We reduce the high-level security of the record layer to cryptographic assumptions on its ciphers. Each step in the reduction is verified by typing an F* module, for each step that involves a cryptographic assumption, this module precisely captures the corresponding game. We first verify the functional correctness and injectivity properties of our implementations of one-time MAC algorithms (Poly1305 and GHASH) and provide a generic proof of their security given these two properties. We show the security of a generic AEAD construction built from any secure one-time MAC and PRF. We extend AEAD, first to stream encryption, then to length-hiding, multiplexed encryption. Finally, we build a security model of the record layer against an adversary that controls the TLS sub-protocols. We compute concrete security bounds for the AES_128_GCM, AES_256_GCM, and CHACHA20_POLY1305 ciphersuites, and derive recommended limits on sent data before re-keying. We plug our implementation of the record layer into the miTLS library, confirm that they interoperate with Chrome and Firefox, and report initial performance results. Combining our functional correctness, security, and experimental results, we conclude that the new TLS record layer (as described in RFCs and cryptographic standards) is provably secure, and we provide its first verified implementation.

Source: https://www.microsoft.com/en-us/research/publication/implementing-proving-tls-1-3-record-layer/

Titan: a custom TPM and more

I listened to a podcast and cut out the chit-chat, so you don’t have to:

Titan is a tiny security co-processing chip used for encryption, authentication of hardware, authentication of services.

Purpose

Every piece of hardware in google’s infrastructure can be individually identified and cryptographically verified, and any service using it mutually authenticates to that hardware. This includes servers, networking cards, switches: everything. The Titan chip is one of the ways to accomplish that.

The chip certifies that hardware is in a trusted good state. If this verification fails, the hardware will not boot, and will be replaced.

Every time a new bios is pushed, Titan checks that the code is authentic Google code before allowing it to be installed.  It then checks each time that code is booted that it is authentic, before allowing boot to continue.

‘similar in theory to the u2f security keys, everything should have identity, hardware and software. Everything’s identity is checked all the time.’

Suggestions that it plays important role in hardware level data encryption, key management systems, etc.

Hardware

Each chip is fused with a unique identifier. Done sequentially, so can verify it’s part of inventory sequence.

Three main functions: RNG, crypto engine, and monotonic counter. First two are self-explanatory. Monotonic counter to protect against replay attacks, and make logs tamper evident.

Sits between ROM and RAM, to provide signature valididation of the first 8KB of BIOS on installation and boot up.

Production

Produced entirely within google. Design and process to ensure provenance. Have used other vendor’s security coprocessors in the past, but want to ensure they understand/know the whole truth.

Google folks unaware of any other cloud that uses TPMs, etc to verify every piece of hardware and software running on it.

Challenges in Authenticated Encryption

Authenticated encryption is the cryptographer’s front-line defense against attackers. It is the
protective shield applied to every network packet. It is the foundation of security for medical
devices, connected vehicles, the financial sector, the smart grid, and the Internet of Things.
But is this shield actually being used? Is it actually working? Is it doing what the users
actually need? Are industry practitioners listening to researchers? Are researchers listening
to industry practitioners?
This white paper identifies critical ongoing problems whose solutions will need concerted
community effort stretching years into the future. The challenges described in this white
paper are classified into four categories:
• Chapter 1: The security target is wrong.
• Chapter 2: The interface is wrong.
• Chapter 3: The performance target is wrong.
• Chapter 4: Mistakes and malice.
This white paper does not mean to suggest that authenticated ciphers are always aiming at
the wrong target. It is important to understand that, for many environments today, using
an existing standard such as AES-128-GCM [19] is simple, safe, and efficient. However, it is
equally important to understand that the existing standards fail to meet the needs of many
other environments. The AES cipher [10] and the AES-GCM authenticated cipher are used
as examples throughout this document to illustrate what can and does go wrong.

Source: https://chae.cr.yp.to/chae-20170301.pdf

AES-GCM-SIV: Specification and Analysis

Abstract. In this paper, we describe and analyze the security of the AES-GCM-SIV mode of operation, as defined in the CFRG specification [10]. This mode differs from the original GCM-SIV mode that was designed in [11] in two main aspects. First, the CTR encryption uses a 127-bit pseudo-random counter instead of a 95-bit pseudo-random value concatenated with a 32-bit counter. This construction leads to improved security bounds when encrypting short messages. In addition, a new key derivation function is used for deriving a fresh set of keys for each nonce. This addition allows for encrypting up to 250 messages with the same key, compared to the significant limitation of only 232 messages that were allowed with GCM-SIV (which inherited this same limit from AES-GCM). As a result, the new construction is well suited for real world applications that need a nonce-misuse resistant Authenticated Encryption scheme. We explain the limitations of GCM-SIV, which motivate the new construction, prove the security properties of AES-GCM-SIV, and show how these properties support real usages. Implementations are publicly available in [8]. We remark that AES-GCM-SIV is already integrated into Google’s BoringSSL library [1], and its deployment for ticket encryption in QUIC [16] is underway.

Source: https://eprint.iacr.org/2017/168.pdf