Understanding Noise*: A Verified Secure Channel Protocol Library

Explore Noise*, a library of high-performance secure channel protocol implementations that have been verified for correctness. The Noise protocol examples, such as IKpsk2, showcase key exchange patterns used in applications like WhatsApp and Wireguard VPN. Discover the importance of verified implementations, available languages (C, Rust, Haskell, Java), and the process of verifying multiple protocols simultaneously.

• Secure Channel Protocol
• Noise*
• Verified Implementations
• IKpsk2
• Security Analysis

luhr633 Follow

Uploaded on Oct 10, 2024 | 0 Views

Download Presentation

Please find below an Image/Link to download the presentation.

The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.

Presentation Transcript

1. Noise*, A Library of Verified High-Performance Secure Channel Protocol Implementations S. Ho, J. Protzenko, A. Bichhawat, K. Bhargavan

2. Noise: Simple DSL for Key-Exchange Protocols Examples of protocol patterns: WhatsApp Wireguard VPN X: IK: IKpsk2: one-way encryption s s s mutual authentication and 0-RTT . . . . . . . . . e, es, s, ss e, es, s, ss e, es, s, ss e, ee, se e, ee, se, psk authenticated server Lightning, I2P NX: XX: XK: e e s e, ee, s, es e, ee, s, es . . . s, se e, es e, ee Today: 59+ protocols (but might increase) s, se 2

3. Noise Protocol Example: IKpsk2 Pattern Initiator Responder IKpsk2: IKpsk2: IKpsk2: IKpsk2: s s s s s: static e: ephemeral Premessages . . . . . . . . . . . . e, es, s, ss, [d0] e, es, s, ss, [d0] e, es, s, ss, [d0] e, es, s, ss, [d0] Early data Handshake Messages (similar to TLS 0-RTT, 0.5-RTT) e, ee, se, psk, [d1] e, ee, se, psk, [d1] e, ee, se, psk, [d1] e, ee, se, psk, [d1] Transport [d2, d3, ] [d2, d3, ] [d2, d3, ] [d2, d3, ] The handshake describes how to: Exchange key material Exchange key material The handshake describes how to: Exchange key material Derive and chain shared secrets (Diffie-Hellman operations ) Derive and chain shared secrets (Diffie-Hellman operations ) Derive and chain shared secrets (Diffie-Hellman operations ) The handshake describes how to: Exchange key material Derive and chain shared secrets (Diffie-Hellman operations ) Send/receive encrypted data Send/receive encrypted data Send/receive encrypted data Send/receive encrypted data The handshake describes how to: 3

4. Unverified Implementations of Noise Noise has many available implementations: In C: Noise-C (github.com/rweather/noise-c) In Rust: Snow (github.com/mcginty/snow) In Haskell: Cacophony (github.com/haskell-cryptography/cacophony) In Java: Noise-Java (github.com/rweather/noise-java) A lot of bugs have been found in protocol implementations (ex.: TLS) None of those implementations is verified! There exists verified implementations of protocols (miTLS, Signal*, ). But how to verify 59 protocols at once? 4

5. What is Noise Noise*? Correctly implemented protocols? Noise* compiler: Noise protocol pattern verified, specialized C implementation On top: complete, verified library stack exposed through a high-level, defensive API Complemented with a formal symbolic security analysis Low-Level Code Formal Specification Security Analysis API Code API Spec API Analysis Noise Protocol Code Noise Protocol Spec Protocol Analysis Crypto Library Crypto Algorithms Symbolic Model Compilation Verify (F*) Verify (DY*) Verified C Code 5

6. How did we implement the Noise* protocol compiler? Low-Level Code Formal Specification Security Analysis API Code API Spec API Analysis Noise Protocol Code Noise Protocol Spec Protocol Analysis Crypto Library Crypto Algorithms Symbolic Model 6

7. What is our toolchain? F* theorem prover F*: general-purpose functional programing language aimed at program verification Low*: effectful subset of F* to write verified C-like code KaRaMeL: framework to compile Low* code to equivalent C code Those tools have been successfully used in the Everest project: Verified cryptographic primitives: Hacl*, ValeCrypt, EverCrypt Verified parsers/serializers: EverParse Verified cryptographic protocols: miTLS, Signal*, QUIC 7

8. A Formal Specification of Noise F* theorem prover F* specification written as an interpreter in a pure, high-level language: let rec send_message_tokens ... (tokens : list message_token) : hsk_state -> result (bytes & hsk_state) = match tokens with | [] -> return empty_bytes | tk :: tokens' -> msg <-- send_message_token ... tk; msg' <-- send_message_tokens ... tokens'; return (msg @ msg') return (msg @ msg') let rec send_message_tokens ... (tokens : list message_token) : hsk_state -> result (bytes & hsk_state) = match tokens with | [] -> return empty_bytes | tk :: tokens' -> msg <-- send_message_token ... tk; msg' <-- send_message_tokens ... tokens'; Clean, auditable code without low-level details (buffers, pointers, etc.) 8

9. How to write verified C code? KaRaMeL: Low* C (inlining, erasure, monomorphization ) Low*: effectful subset of F* modelling C // Generated C code Void aead_encrypt(uint8_t *key, ...) { encrypt(mlen, cipher, m, key, n, (uint32_t)1U); uint8_t tmp[64U] = { 0U }; encrypt((uint32_t)64U, tmp, tmp, key, n, (uint32_t)0U); uint8_t *key = tmp; poly1305_do_32(key, aadlen, aad, mlen, cipher, mac); } // Low* signature val aead_encrypt : key:lbuffer uint8 32ul -> ... -> Stack unit (requires (fun h0 -> live h0 key /\ disjoint key output /\ ... )) Pre (ensures (fun h0 _ h1 -> modifies2 output tag h0 h1 /\ ... )) Post // Low* implementation let aead_encrypt key n aadlen aad mlen m cipher mac = chacha20_encrypt mlen cipher m key n 1ul; derive_key_poly1305_do key n aadlen aad mlen cipher mac Type-checked requires (precondition): non-dangling pointers, disjointness ensures (postcondition): which buffers are modified, functional correctness (Low* code refines high-level spec) when type-checking the body: proof obligations generated and sent to Z3 SMT solver Low* has been successfully used for: cryptographic primitives (Hacl*, EverCrypt ) protocols (miTLS, QUIC, Signal* ) We can verify and implement one protocol How do we verify 59 at once? 10

10. Generic Interpreter vs Specialized Implementation We can write an interpreter for Noise in Low*: WireGuard VPN (IKpsk2): let rec send_message_tokens initiator is_psk tokens st out_len out : error_code = match tokens with | Nil -> 0ul | tk :: tokens' -> let tk_outlen = token_message_length tk in let tk_out = sub out 0ul tk_outlen in let r1 = send_message_token initiator is_psk tk st tk_out in if is_success r1 then begin let outlen' = outlen - tk_outlen in let out' = sub out tk_outlen outlen' in send_message_tokens initiator is_psk tokens' st outlen' out' end else r1 /* First message: e, es, s, ss */ hsk_init(hsk->chaining_key, hsk->hash, hsk->remote_static); /* e */ curve25519_generate_secret(hsk->ephemeral_private); if (!curve25519_generate_public(dst->unencrypted_ephemeral, hsk->ephemeral_private)) goto out; message_ephemeral(dst->unencrypted_ephemeral, dst->unencrypted_ephemeral, hsk->chaining_key, hsk->hash); /* es */ if (!mix_dh(hsk->chaining_key, key, hsk->ephemeral_private, hsk->remote_static)) goto out; /* s */ message_encrypt(dst->encrypted_static, hsk->static_identity->static_public, NOISE_PUBLIC_KEY_LEN, key, hsk->hash); Specialized, idiomatic C code: no recursion, no list of tokens, etc. Interpreter, recursive over the list of tokens /* ss */ if (!mix_precomputed_dh(hsk->chaining_key, key, hsk->precomputed_static_static)) How to specialize an interpreter for a given input? How to turn an interpreter into a compiler? goto out; 11

11. Compilation Through Partial Evaluation Process 1st message of IKpsk2 as initiator (simplified): let send_IKpsk2_message0 st out_len out : error_code = let tk_outlen = token_message_length E in let tk_out = sub out 0ul tk_outlen in let r1 = send_message_token true E st tk_out in if is_success r1 then begin let outlen' = outlen - tk_outlen in let out' = sub out tk_outlen outlen' in send_message_tokens true true [ES; S; SS] st outlen' out' end end end else r1 else r1 | ES -> send_message_ES true true st tk_out | ES -> send_message_ES true true st tk_out | PSK -> send_message_PSK true true st tk_out end begin begin let outlen' = outlen - 32 in let out' = sub out 32 outlen' in send_message_tokens true true [ES; S; SS] st outlen' out' end else r1 else r1 else r1 Partial evaluation combined with F* s powerful type system generates very specialized code, with: let send_IKpsk2_message0 st out_len out : error_code = send_message_tokens true true [E; ES; S; SS] st out_len out send_message_tokens true true [E; ES; S; SS] st out_len out match [E; ES; S; SS] with | Nil -> 0ul | tk :: tokens' -> let tk_outlen = token_message_length tk in let tk_out = sub out 0ul tk_outlen in let r1 = send_message_token true true tk st tk_out in if is_success r1 then begin let outlen' = outlen - tk_outlen in let out' = sub out tk_outlen outlen' in send_message_tokens true true tokens' st outlen' out' end else r1 else r1 if is_success r1 then begin let outlen' = outlen - 32 in let out' = sub out 32 outlen' in send_message_tokens true true [ES; S; SS] st outlen' out' end else r1 else r1 Specialized types let send_IKpsk2_message0 st out_len out : error_code = let tk_outlen = token_message_length E in let tk_out = sub out 0ul tk_outlen in let r1 = send_message_token true E st tk_out in if is_success r1 then begin let outlen' = outlen - tk_outlen in let out' = sub out tk_outlen outlen' in send_message_tokens true true [ES; S; SS] st outlen' out' end else r1 else r1 else r1 else r1 | PSK -> send_message_PSK true true st tk_out end end else r1 let outlen' = outlen - 32 in let out' = sub out 32 outlen' in send_message_tokens true true [ES; S; SS] st outlen' out' end else r1 else r1 No recursion (evaluated away) No lists of tokens (evaluated away) Precise control-flow (no unnecessary dynamic checks) let send_IKpsk2_message0 st out_len out : error_code = let tk_out = sub out 0ul 32 in let r1 = begin match E with in if true then // if is_psk if true then // if is_psk mix_key st.ephemeral st.symmetric_state; mix_key st.ephemeral st.symmetric_state; mix_key st.ephemeral st.symmetric_state; update out 0ul st.ephemeral; update out 0ul st.ephemeral; let send_IKpsk2_message0 st out_len out : error_code = let tk_out = sub out 0ul 32 in let r1 = send_message_token true E st tk_out in if is_success r1 then begin let outlen' = outlen - 32 in let out' = sub out 32 outlen' in let out' = sub out 32 outlen' in | SS -> send_message_SS true true st tk_out | SS -> send_message_SS true true st tk_out begin () () in if is_success r1 if is_success r1 if true then begin let outlen' = outlen - 32 in let out' = sub out 32 outlen' in let send_IKpsk2_message0 st out_len out : error_code = let send_IKpsk2_message0 st out_len out : error_code = let send_IKpsk2_message0 st out_len out : error_code = match [E; ES; S; SS] with | Nil -> 0ul | tk :: tokens' -> let tk_outlen = token_message_length tk in let tk_out = sub out 0ul tk_outlen in let r1 = send_message_token true true tk st tk_out in if is_success r1 then begin let outlen' = outlen - tk_outlen in let out' = sub out tk_outlen outlen' in send_message_tokens true true tokens' st outlen' out' end in in if is_success r1 then begin let outlen' = outlen - 32 in let out' = sub out 32 outlen' in send_message_tokens true true [ES; S; SS] st outlen' out' end let send_IKpsk2_message0 st out_len out : error_code = let tk_outlen = 32 in let tk_out = sub out 0ul tk_outlen in let r1 = send_message_token true E st tk_out in if is_success r1 then begin let outlen' = outlen - tk_outlen in let out' = sub out tk_outlen outlen' in send_message_tokens true true [ES; S; SS] st outlen' out' send_message_tokens true true [ES; S; SS] st outlen' out' end end | SE -> send_message_SE true true st tk_out | SE -> send_message_SE true true st tk_out let out' = sub out 32 outlen' in send_message_tokens true true [ES; S; SS] st outlen' out' then then begin let outlen' = outlen - 32 in let out' = sub out 32 outlen' in send_message_tokens true true [ES; S; SS] st outlen' out' end end end let send_IKpsk2_message0 st out_len out : error_code = let tk_out = sub out 0ul 32 in let tk_out = sub out 0ul 32 in let tk_out = sub out 0ul 32 in let tk_out = sub out 0ul 32 in let tk_out = sub out 0ul 32 in let send_IKpsk2_message0 st out_len out : error_code = let tk_out = sub out 0ul 32 in let r1 = begin match E with | S -> send_message_S true true st tk_out | S -> send_message_S true true st tk_out if is_success r1 mix_key st.ephemeral st.symmetric_state; mix_key st.ephemeral st.symmetric_state; update out 0ul st.ephemeral; update out 0ul st.ephemeral; () () () let send_IKpsk2_message0 st out_len out : error_code = let tk_out = sub out 0ul 32 in let r1 = send_message_token true E st tk_out in if is_success r1 then begin let outlen' = outlen - 32 in | E -> send_message_E true true st tk_out | E -> send_message_E true true st tk_out then update out 0ul st.ephemeral; update out 0ul st.ephemeral; () in in in in let outlen' = outlen - 32 in let out' = sub out 32 outlen' in send_message_tokens true true [ES; S; SS] st outlen' out' let send_IKpsk2_message0 st out_len out : error_code = let send_IKpsk2_message0 st out_len out : error_code = let send_IKpsk2_message0 st out_len out : error_code = let send_IKpsk2_message0 st out_len out : error_code = let send_IKpsk2_message0 st out_len out : error_code = let tk_out = sub out 0ul 32 in let r1 = send_message_E true true st tk_out mix_hash st.ephemeral st.symmetric_state; mix_hash st.ephemeral st.symmetric_state; mix_hash st.ephemeral st.symmetric_state; mix_hash st.ephemeral st.symmetric_state; mix_hash st.ephemeral st.symmetric_state; mix_hash st.ephemeral st.symmetric_state; mix_key st.ephemeral st.symmetric_state; let send_IKpsk2_message0 st out_len out : error_code = let tk_out = sub out 0ul 32 in let r1 = let r1 = let r1 = let r1 = let r1 = let r1 = let send_IKpsk2_message0 st out_len out : error_code = let tk_outlen = 32 in let tk_out = sub out 0ul tk_outlen in let r1 = send_message_token true E st tk_out in if is_success r1 then begin let outlen' = outlen - tk_outlen in let out' = sub out tk_outlen outlen' in send_message_tokens true true [ES; S; SS] st outlen' out' send_message_tokens true true [ES; S; SS] st outlen' out' | EE -> send_message_EE true true st tk_out | EE -> send_message_EE true true st tk_out let outlen' = outlen - 32 in in if is_success r1 if is_success r1 then then begin let outlen' = outlen - 32 in let out' = sub out 32 outlen' in send_message_tokens true true [ES; S; SS] st outlen' out' send_message_tokens true true [ES; S; SS] st outlen' out' 12

12. Verified Meta Programming Idea: use F* to meta-program as much as possible: Similar to super advanced C++ templates Write a meta-program once, specialize N times ( 59 patterns) Technique: Futamura projection Historically, long arc of meta-programming in F*: EverCrypt agility (2020) HACLxN vector types (2021) Streaming Functor (2021) EverParse (2019-now) Very useful to factorize cryptographic code (MD hash functions, generic/optimized implementations, etc.) With Noise*: complete, meta-programmed protocol stack 13

13. Security Analysis Low-Level Code Formal Specification Security Analysis API Code API Spec API Analysis Noise Protocol Code Noise Protocol Spec Protocol Analysis Crypto Library Crypto Algorithms Symbolic Model 14

14. Generic Security Analysis in DY* Noise defines authentication and confidentiality levels: IKpsk2: Auth. Conf. s . . . e, es, s, ss, [d0] 1 2 e, ee, se, psk, [d1] 2 4 [d2] 2 5 [d3] 2 5 We formalize the Noise security levels as security goals in DY*, a framework for symbolic analysis developed in F*. We do one generic symbolic security proof at the level of the interpreter spec. 15

15. What does the high-level, defensive API give us? Low-Level Code Formal Specification Security Analysis API Code API Spec API Analysis Noise Protocol Code Noise Protocol Spec Protocol Analysis Crypto Library Crypto Algorithms Symbolic Model Verified, meta-programmed state machines Misuse resistant API which reflects security guarantees Key & peer management 16

16. High-Level, User-Friendly, Defensive API Verified, meta-programmed state machines: Protocol transitions are low-level (a lot of bugs in TLS) Abstract away handshake messages, transition to transport phase: send_message, recv_message Misuse resistant API that reflects security guarantees: Dynamically check that we don t send secret messages too early Propagate security proofs in the API IKpsk2: s . . . Key & peer management: Remote key validation Load/store static keys PSK lookup Secure storage on disk e, es, s, ss, [d0] e, ee, se, psk, [d1] [d2, d3, ] In most implementations: high-level API is the biggest component (3/4 of LoCs for Noise*) 17

17. Performance We generated 59 patterns * 8 cipher suites = 472 instantiations of the API 1 instantiation = 4k to 6k lines of C code Performance Comparison, in hsks / second. Benchmark performed on a Dell XPS13 laptop (Intel Core i7-10510U) with Ubuntu 18.04 18

18. Conclusion We introduced Noise*, whichis: A compiler from Noise protocol patterns to efficient, verified C code, executed in F* normalizer A complete, verified library stack exposed through a high-level, defensive API A symbolic security analysis generically performed on protocol and API Noise* showcases techniques useful to: Verify full software stacks Automate production of code where we don t sacrifice precision or performance F* source code and generated C code available on github: github.com/Inria-Prosecco/noise-star Pick one of 472 generated instantiations of Noise (IKpsk2_25519_ChaChaPoly_BLAKE2b, ) If you need a specific choice of (optimized) primitives: son.ho@inria.fr Questions? 19