Three ways formal methods can scale for software security
Security is not like paint: it can’t just be applied after a system has been completed. Instead, security has to be built into the system design. But how can we know that a system design is secure against a particular attack? And how can we know that the system implements that design correctly?
The key problem, on one hand, is that system design specifications are often ambiguous and incomplete, with specifications (if they exist at all) intended for human consumption and reasoning. On the other hand, system implementations are often highly complex, evolving over time, and often diverging from design specifications as they evolve. In the resulting landscape, defects can easily creep into the design, and implementation both allows them to persist and introduces new ones.
Consider, for example, TLS – the protocol widely used to secure internet traffic between web browsers and servers. In recent years, TLS has suffered from damaging attacks against both its state machine design and its implementation in the OpenSSL library.
The standard approach to flushing out design and implementation defects is testing. Test early, test often, check your test coverage. But tests only cover a tiny fraction of the input and state space of real software applications – the fraction that test developers can imagine when they sit down to write tests. It’s normal for even well-tested software to ship with defects that must be remedied later. Those test-resilient defects show that testing – guessing – isn’t the same as knowing the security stance of your software.
How can we know the security stance of software today, with practical methods? Security conscious developers are increasingly turning to a new approach: formal methods (FM).
FM is a type of mathematical modelling where the system design and code are the subjects of the model. By applying mathematical reasoning, FM tools can answer security questions with mathematical certainty. For example, FM tools can determine whether a design has lurking security issues before implementation begins; show that an implementation matches the system design; and prove that the implementation is free of introduced defects such as low-level memory errors. That certainty distinguishes FM from other security technologies: unlike testing and fuzzing, which can only trigger a fraction of all system executions, an FM model can examine every possible system behavior.
Formal methods in production
Like machine learning, the roots of formal methods lie in the 1970s, and also like machine learning, recent years have seen rapid adoption of FM technologies. Modern FM tools have been refined by global-scale companies like Microsoft, Facebook, and Amazon. As a result, these tools reflect the engineering practices of these companies: rapid pace of iteration, low cost of entry, and interoperability between many complementary tools.
One of the first successes for modern FM was Microsoft’s Static Driver Verifier. Errors in device drivers are inherently a source of security risk, and Microsoft tackled this problem by building an FM tool that checks that the driver correctly interacts with the Windows kernel. This tool is shipped as part of Visual Studio, meaning that every vendor could ensure their code was secure. The Static Driver Verifier raised the bar for device drivers by making the highest standards of security available to everyday developers.
Facebook uses FM to prevent crashes and security bugs across its C and Java codebases. Facebook’s Infer tool analyses each commit to a protected codebase and raises the alarm if an error is possible. Key to the success of this tool is its ability to focus on just the code that has changed in each commit. Unlike standard testing, this means that a code reviewer can know precisely whether a new bug has been introduced. Infer also demonstrates how FM can complement standard CI/CD workflows.
Amazon Web Services uses FM to ensure its cryptographic systems are secure. For performance reasons, cryptographic operations are heavily optimized, and this makes it difficult to be confident the software matches its mathematical design. Amazon uses an FM tool called SAW to guarantee the two correspond, which removes a source of critical security bugs. SAW also monitors commits to cryptographic operations, ensuring that bugs cannot be introduced. This shows how FM can be applied surgically to generate confidence at critical points in a system.
From promising beginnings to scalable practicality
Although these success stories prove that FM can let you know your security stance with mathematical certainty, they don’t prove the practicality of FM in production environments. The rap on formal methods is that it is only feasible for complex, mission-critical environments where organizations can invest significant time and resources.
For example, NIST notes that in the early days, formal methods “developed a reputation as taking far too long, in machine time, person years and project time, and requiring a PhD in computer science and mathematics to use them.”
However, the story for practicality and scalability of FM has changed. Current and emerging FM re-imagines the ways FM tools can be practically applied to a broad range of software projects. Adoption of these few key principles behind this new wave of FM is resulting in consistent success across an increasing community of companies:
Don’t view FM as an “all or nothing” proposition
Some organizations considering formal methods shy away because they assume it is an “all or nothing” endeavor. There is a common perception that you have to verify an entire system (which may be a slow and expensive proposition, or even impossible). Successful organizations are thinking of FM as simply another tool in the toolbox to gain confidence in software and systems. One or many FM tools may be the right fit to deliver value in your development workflow.
Choose wisely when it comes to FM precision vs. scale
Formal methods in principle can verify almost any property about a piece of software, but real tools must trade precision against the scale of the software. Modern formal methods have solved this dilemma by developing a range of tools appropriate for different scenarios.
Precise tools are appropriate for high-risk components that depend on complex internal logic: for example, cryptographic modules and parsers. Scalable tools can be used to assure almost any piece of code, but they can only identify crashes and other simple bugs such as memory safety violations. Choosing the right tool is key to achieving your assurance aims.
Pick the right FM tools for your specific needs
Scaling formal methods will be greatly aided by improving awareness of the various tools available and which tools are best for your organization. Heavyweight tools typically provide formal verification, meaning a mathematical assurance that a system works only as defined in a mathematical model. Amazon has applied the formal verification tool SAW to aspects of s2n, its TLS library protecting AWS.
Middleweight tools include symbolic testing tools such as CBMC and network analysis tools such as Amazon’s Tiros tool. These provide assurance that key properties hold, but don’t model every desired property of the system.
Static analysis is a lightweight option for FM that is gaining popularity due to its accessibility and cost feasibility. Facebook Infer Static Analyzer and Google Error Prone are examples of push button static analysis tools that can be easier to deploy rapidly. Lightweight tools can benefit fast growing but relatively small cloud providers that don’t have FM teams like we are seeing at Facebook, Google and Amazon. It is the proverbial build (harder) vs. deploy (easier) proposition that organizations considering FM will need to evaluate.
FM is ready to serve
The value of knowing is priceless when it comes to security. FM technology means that this knowledge can be had today at the critical points in your systems. Modern FM is designed for production engineering environments, with a range of proven tools, and more being developed every month. Where you need to know, FM is ready to serve.