Dependent Types in Protocol Security Analysis
Alessandro Bruni, a computer scientist specializing in computer security and software verification, discusses the use of refinement types and F* in proving the security of protocols. He highlights the power of expressing data properties with types, showcasing examples and emphasizing the importance of rigorous verification methods like miTLS. The concept of Security Games is introduced as a strategic approach to ensuring protocol security against attackers through game-based analysis. Various security vulnerabilities and their prevention strategies are also explored in this informative presentation.
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.
E N D
Presentation Transcript
Verified protocol implementations in F* Alessandro Bruni
$ whoami # Alessandro Bruni Computer Scientist Now: Postdoc researcher @ ITU (computer security, SW verification, theorem provers ) Before: Fall 2015: Garbage Collector @ Prolog Dev. Center 2012-2015: PhD @ DTU (computer sec., SW ver, ...) Contributed crypto examples to the FStar repo 2012: Research Eng. @ Siav SpA (process mining) Find me at: alessandrobruni.name / @hoheinzollern
Recap: F* & Refinement types F* = F# + Types on Steroids: + = Can express powerful properties on data, e.g.: val cons: n: nat -> l: a list {n = List.length l} -> x: a -> l : a list {n+1 = List.length l } Can we use refinement types for proving security of protocols?
Could /that/ be prevented? 1. Yes 2. Yes! Like tons of similar vulnerabilities, using a strong typing discipline Option 2: val reply: len:nat -> msg:text{length msg = len} -> resp:text{resp = msg} Hint: not a complete solution
miTLS: A Verified Reference Implementation of TLS Uses F* dependent types to reason about the security of TLS Attacks discovered while verifying TLS: Alert 3SHAKE VHC SMACK Logjam SLOTH Quick morale: Automatic reasoning about program correctness helps to discover problems, otherwise unnoticed The more automatic checking, the better
Introducing: Security Games the only winning move is not to play Artificial setup: Attacker given access to an Oracle, who gives him lots of information (e.g. encrypts/decrypts messages for him) minus some important bits (e.g. encryption keys) Game follows a script: the attacker and the oracle both follow the rules of the game Security proof: If the attacker has no better strategy than purely random guesses then the protocol is secure
Eavesdropping security (EAV) Oracle (knows k) Eavesdropper m[0] m[1] ( , ) b = sample {0,1} encrypt(k, m[b]) guess b Eavesdropper wins the game if P(guess b) > +
Uppin the Game: Chosen Plaintext Attacks (IND-CPA) m[0] m[1] ( , ) b = sample {0,1} encrypt(k, m[b]) guess b We give the attacker access to encrypt(k, -) before and after the interaction with the user Still, we should have P(guess b) < + Encryption should never return the same value twice ;)
Integrity of Chosen Message Attacks (INT-CMA) Oracle (knows k) Attacker m t = sign(k, m) (m , t ) t = sign(m , k) Attacker can query the oracle for signatures, but each requested message m is logged along with its signature tag t The attacker wins the game if he can produce a new pair (m , t ), where t = sign(k, m ), with probability >
Reasoning in F* Security games are recipes (programs?) Involve interaction between parties val send: string -> IO unit val recv: unit -> IO string Express verification conditions IND-CPA Encryption: val enc: k:key -> plain -> c:cipher{Encrypted k c} val dec: k:key -> c:cipher{Encrypted k c} -> plain INT-CMA Signatures: val mac: k:key -> t:text{Oracle k t} -> tag val verify: k:key -> t:text -> tag -> b:bool{b ==> Oracle k t} Are we missing something?
Introducing: Probabilistic F* New construct: let n = sample {0,1} in n = 1 50% 50% n = 0
Negligible differences let mac k t = let m = hmac_sha1 k t in log := Entry k t m :: !log; m let mac k t = let m = hmac_sha1 k t in m < let verify k text tag = let m = hmac_sha1 k text in let verified = (m = tag) in let found = is_Some (List.find (fun (Entry k' text' tag ) -> k = k' && text = text') !log) in let verify k text tag = let m = hmac_sha1 k text in let verified = (m = tag) in verified verified && found Remember: val mac: k:key -> t:text{Oracle k t} -> tag val verify: k:key -> t:text -> tag -> b:bool{b ==> Oracle k t}
Example: RPC protocol A -> B: utf8 s, mac kAB s B -> A: utf8 t, mac kAB (s, t) assume forall k t . Oracle k (utf8 t) <==> Request t let client q = assume Request(q) ... send mac k (utf8 q) let server q = ... if verify k (utf8 q) m then assert Request(q) process q
Conclusions We can build cryptographic proofs of correctness using dependent types Precisely reasoning about the correctness of programs (using types) helps discover problems (miTLS attacks) Interested in more crypto protocols? Explore /FStar/examples/crypto
