Formal proofs vs. security ========================== Paper: "Formal Proofs, the Fine Print and Side Effects" Toby Murray and P.C. van Oorschot IEEE SecDev 2018 "Best Practices" (BP) paper: clarifying a major security area. Why this paper? Security is a big motivation for formal verification. Adversary may be able to take advantage of corner cases. .. more so than "randomness" in concurrent or distributed systems. Proofs are an appealing way to ensure no corner cases are missed. How do formal proofs actually relate to security in practice? Gaps in applying formal results to deployed systems. How to think about the value of proofs, even if they are not perfect? Undesirable side-effects from formal methods. No new results in this paper; instead, brings up interesting issues. Different ways of thinking about why proofs might be helpful. Interesting perspective from Toby Murray (co-author on many seL4 papers). Some repeating themes w/ earlier papers about the value of proofs. Amazon (not going all the way to full proofs). Distributed system case study (proofs seem to work, for proven parts). Why proofs for security? Precise statement. Machine-checked to avoid human errors in code. No bugs that violate spec. As long as theorem captures what we want, code doesn't matter. Why not proofs for security? Security statement might be quite technical and hard to understand E.g., from paper: Benjamin Pierce took a full week to understand seL4 theorem. This guy knows what he's doing: primary author of Software Foundations. Formal assumptions might be not quite right. E.g., not a precisely accurate model of underlying hardware. Missing timing information from CPU execution model? Paper example: restricted model of ARM non-determinism. Paper example: missing certain instructions or registers from CPU model. Attackers often go around the well-understood defenses. Take advantage of unspecified aspects of system. Side channels, extra instructions, debug/development modes, mgmt modes, .. Physical features/defects like Rowhammer, RAMbleed. Hardware has bugs: Intel publishes hundreds of "errata" documenting issues. No formal models of x86 that I know about actually include all these errata. Physical access to a device: under-volting, resetting, etc. Take advantage of human users -- e.g., phishing for credentials. Circumvent the theorem in other ways. Proofs take time away from doing more useful things. Lots of time spent on proving, could have been spent on something else? Fuzzing. Audits. Rewriting code to be cleaner, better isolated. Proofs might cause developers to write code that's less secure. Hypothetical possibility in the paper, but something to keep in mind. Our own anecdode: we got sloppy about off-by-one errors in FSCQ, because we expected the proofs will catch things. (And they did, in that case.) Formal verification is much easier when code is written in a certain style. That style might be at odds with otherwise writing clear, simple code. E.g., having to write code in a functional style, extraction, etc. Could be that writing this stylized code makes it more error-prone. Worst case: errors might be in aspects that aren't captured by theorem. Important to have an accurate threat model. But formal methods demand an extremely precise threat model. Unrealistic to expect we will get it right. What's the value of the proof if the model isn't right? Paper's view in terms of Venn diagrams. Change needed for verification? No Yes (P) | No | Change fixes | security issue? -----------------+---------------------- | Yes (A) | | Figures 2-5 in the paper try to describe how many things are in each quadrant Another dimension: changes that introduce a security issue not covered by spec? "V" Quite unfortunate if these showed up in the "P" column. If this were significant, verification could lead to worse code. Breakout Q: what has your experience been with verification (e.g., in labs)? Where are your code changes? Lots of changes to make verification happy but not relevant to correctness? Real bugs fixed due to verification? More error-prone code in some way due to verification? Paper: several ways of looking at why proofs are useful. Qualified guarantees. Forces a precise threat model. Conditional statement about correctness / security. But might be hard to tease out the qualifications of guarantee. Benjamin Pierce example from above. Also hard to figure out the implications of some qualification. E.g., not-quite-accurate model of ARM ISA w.r.t. "unpredicable" behaviors. Need to be quite an expert to know this is OK for functional correctness, but not OK for confidentiality / non-interference theorems. Odd form of "qualified guarantee": changing code/protocol to make the proof work. E.g., WireGuard example from the paper. Verification researchers had to make a small change to protocol to verify it. Unclear if it's a limitation of the proof technique, or real protocol bug, or perhaps some missing assumption? Perhaps value of proof is demonstrating certain proof techniques, which can be used to verify real protocols. Or perhaps in proving that other aspects of the protocol are secure. Probabilistic guarantees? Not a good fit: adversary not probabilistic. Structured exploration. Forces developers to think carefully. Relates to Butler's point from earlier in the class: diminishing returns. Write down the state. Write down the specification. Write down the abstraction relation. Do the proof. Doing the proof forces all of the previous steps to be done correctly. But much of the value comes from the earlier steps, if done correctly. Marketing / regulatory. Not much said in the paper. Some real-world examples: e.g., Bedrock Systems; seL4. Downsides of proofs. Significant effort; better spent elsewhere? Clumsy code? Clumsy interaction with non-verified code? Saw several examples of this in the distributed systems case study paper. Shim layer has many bugs. Not clear whether these bugs would be there or not, if not for verification. Brittle code? Paper argues that verified code is brittle: changing code breaks proof. True but probably not any more brittle than regular code in that sense. One potential concern is maintainability, though. Example from verified crypto in Firefox: developers wanted verified code to produce normal-looking C code, so they can edit it in the worst case. Would be bad if verification prevents the code from evolving. Over-reliance on one defense strategy? E.g., Java VM or Javascript VM provably enforce memory safety. No need for ASLR, etc? Hardware bit-flips (e.g., Rowhammer) can violate assumptions about memory. Allows adversarial code to leverage bit flips to escape from "memory-safe" VM. Important to have "defense in depth" in practice. Mitigation for the possibility of getting the threat model wrong. Open questions on the verification front: Partial proofs? What does it mean to verify some code embedded in a larger unverified system? Theorems that quantify the precise assumptions necessary for theorem to hold? What's the most effective way to build reliable / secure systems? Full verification; Amazon-style specs; Fuzzing; Bug-finding tools? Summary Formal methods and proofs do seem to be helpful for correctness / security. Useful to think about why that is -- not a strict logical conclusion. Helps think about formal methods vs. other ways to improve security / reliability. Think of the "downsides" as pitfalls to avoid when doing formal verification.