− author: - Nicolas Pouillard

- IT University of Copenhagen date: 2013-12-28, 30c3, Hamburg css: - reveal.js/css/theme/solarized.css - breach.css --- # BREACH in Agda ## BREACH

SSL, GONE IN 30 SECONDS
* **B**rowser **R**econnaissance &
**E**xfiltration via **A**daptive
**C**ompression of **H**ypertext
* A compression side-channel attack against HTTPS

(through HTTP compression)

## Agda
* A dependently typed functional programming language:
* Functions are dependently types
* Pure (side effect-free)
* Exhaustively defined
* Guaranteed to terminate
* A proof assistant for a powerful logic:
* A unified environment for proofs and programs
* Curry Howard:
* Propositions as Types
* Proofs as Programs
* Backed by Computational Content:
* Witnesses are constructed
* No axiomatization required
# crypto-agda(through HTTP compression)

https://github.com/crypto-agda(Joint work with Daniel Gustafsson) ## Why Crypto? Privacy is a critical issue! Proofs should be fully verified! ## Why Agda? * Functional programming everywhere: * Exploration functions: summations & brute-force * Persistent data by default * Functions are deterministic and exhaustive by default * Processes are expressed by pure functions * Dependent types everywhere: * Precise types for machines and humans * Convenient in the code * Pervasive in the proofs * Type theory everywhere: * Type isomorphisms on Σ-types to prove equality on sums * Protocols as a type-universe * Process type as a decoding of protocols * Randomized function & Probabilistic reasoning # Agda Demo # Security notions, proofs and attacks using dependently typed functional programming ## Public Key Encryption * Each participant generates a key pair: * The _private-key_ **`sk`** is kept secret and never disclosed * The _public-key_ **`pk`** is widely distributed in association with user′s identity * Alice wants to send a private message **`m`** to Bob: * Alice obtains Bob′s public-key * Encryption **`Enc pk m`** produces a _cipher-text_ **`c`** * Alice sends **`c`** to Bob * Decryption **`Dec sk c`** re-produces the message **`m`** * Only Bob knows his private key and thus message was private ## Security notions * IND-CPA: Indistinguishability under chosen-plaintext attack

# Encryption

+

Compression

=

? ## Compression AFTER Encryption? Useless!

Compression after encryption is fruitless, since encrypted data looks like random, and random can't be well compressed. ## Encryption AFTER Compression = ♥ ? ```{.haskell} CEnc : PubKey → Message → Rₑ → CipherText CEnc pk m rₑ = Enc pk (compress m) rₑ ``` Brök3n‼ ## Compression Oracle ### Attack: ```{.haskell} module Compression-Oracle (rₐ : Rₐ) (pk : PubKey) where m : Message ² -- m₀ and m₁ have to be of the same size while -- compress to a different size b′ : CipherText → Bit b′ c = size c == size (CEnc pk m₁ rₐ) ``` ### Proof sketch: ```{.haskell} b′ (CEnc pk (m b) rₑ) ≡ size (CEnc pk (m b) rₑ) == size (CEnc pk m₁ rₐ) ≡ size (Enc pk (compress (m b)) rₑ) == size (Enc pk (compress m₁) rₐ) ≡ size (compress (m b)) == size (compress m₁) ≡ b == 1 ≡ b ``` ## Compression side-channel attack * Assume any compression scheme, which: * Can map two messages of the same size to compressed messages of different size. * Assume any encryption scheme, which: * Is IND-CPA secure. * Leaks the size of the plain-text message. * Cipher text size does not depend on the randomness. ## CRIME > At ekoparty 2012, Thai Duong and Juliano Rizzo announced CRIME, a compression side-channel attack against HTTPS. An attacker with the ability to: > > * Inject partial chosen plaintext into a victim's requests > * Measure the size of encrypted traffic > > can leverage information leaked by compression to recover targeted parts of the plaintext. # BREACH ## BREACH > BREACH (Angelo Prado, Neal Harris, Yoel Gluck) is a category of vulnerabilities and not a specific instance affecting a specific piece of software. To be vulnerable, a web application must: > > * Be served from a server that uses HTTP-level compression > * Reflect user-input in HTTP response bodies > * Reflect a secret (such as a CSRF token) in HTTP response bodies ## BREACH Overview ``` GET /owa/?ae=Item&t=IPM.Note&a=New&id=canary=

My mockup does __not__ address any of those, yet. ## Future work * Verifying voting schemes: Helios, Prêt-à-Voter, Mixnets... * And the required dependencies: * Homomorphic encryption * Non-interactive Zero-knowledge proofs (NIZK) * Naor-Young transform (IND-CPA+NIZK → IND-CCA2) * ... # Thanks!