6.1 KiB
| readstatus | dateread | title | year | authors | citekey | journal | volume | issue | pages | |||
|---|---|---|---|---|---|---|---|---|---|---|---|---|
| false | The HACMS program: using formal methods to eliminate exploitable bugs | 2017 |
|
fisherHACMSProgramUsing2017a | Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences | 375 | 2104 | 20150401 |
Indexing Information
DOI
ISBN
Tags:
[!Abstract] For decades, formal methods have offered the promise of verified software that does not have exploitable bugs. Until recently, however, it has not been possible to verify software of sufficient complexity to be useful. Recently, that situation has changed. SeL4 is an open-source operating system microkernel efficient enough to be used in a wide range of practical applications. Its designers proved it to be fully functionally correct, ensuring the absence of buffer overflows, null pointer exceptions, use-after-free errors, etc., and guaranteeing integrity and confidentiality. The CompCert Verifying C Compiler maps source C programs to provably equivalent assembly language, ensuring the absence of exploitable bugs in the compiler. A number of factors have enabled this revolution, including faster processors, increased automation, more extensive infrastructure, specialized logics and the decision to co-develop code and correctness proofs rather than verify existing artefacts. In this paper, we explore the promise and limitations of current formal-methods techniques. We discuss these issues in the context of DARPA’s HACMS program, which had as its goal the creation of high-assurance software for vehicles, including quadcopters, helicopters and automobiles. This article is part of the themed issue ‘Verified trustworthy software systems’.
[!note] Markdown Notes None!
[!seealso] Related Papers
Annotations
[!attention] Highlight o a first approximation all computers are networked. Even many systems that are supposedly air-gapped are periodically connected, often via USB keys, so their software can be updated.
[!attention] Highlight They created a digital version of a song that played perfectly on a PC but that enabled remote code execution when it played on the particular CD player in the car. The digital encoding of the song contained extra information that triggered a buffer overflow on the car’s CD player.
[!attention] Highlight increased automation, much of which has its roots in the seemingly simple problem of Boolean satisfiability, usually called SAT.
[!attention] Highlight In general, the SAT problem is NP-Complete, meaning the only known solution is to enumerate every possible truth assignment.
[!attention] Highlight SAT solvers form only the most basic level of automation in formal-methods tools. SMT (Satisfiability Modulo Theories) solvers [24] add the ability to automatically reason about higher level structures such as integers, vectors and arrays. Tactic libraries allow interactive theorem provers to automate parts of the proof construction process [25].
[!attention] Highlight A fourth reason is more subjective. Critical systems are reaching a level of complexity that makes it apparent that more advanced tool support is necessary. For example, system developers at Amazon Web Services started using model checking to reason about their distributed systems: We have found that testing the code is inadequate as a method to find subtle errors in design, as the number of reachable states of the code is astronomical. So we looked for a better approach [26]. They point out that human intuition is poorly suited to reasoning about extremely rare ‘once in a million’ kinds of events, but such events happen every second in systems as large as Amazon Web Services. Formal methods help find the strange corner cases and allow designers to decide what to do in those cases.
[!attention] Highlight n the security tests, the Red Team started with full knowledge of the system and its source code. In this phase, not only were they tasked with remotely breaking into the vehicles, but they were also asked to conduct a much more stringent security test. Specifically, they were given root access to the Linux partition, which communicated with multiple hardware components. This access enabled the Red Team to insert whatever code they wanted into the Linux partition and have it run with administrator privileges. Clearly they would be able to disrupt the vision application. The question was whether they could do worse. At the end of six weeks, the Red Team reported they were unable to break into the vehicle remotely. More significantly, even with root access to the Linux partition, they were unable to break out of their partition or disrupt the operation of the vehicles in any way. In a particularly dramatic test, the Red Team launched a full-scale cyber-attack from their onboard vantage point on the SMACCMPilot while it was flying. As expected, the unprotected vision application was totally destroyed, but all flight-critical functionality remained unaffected.
[!attention] Highlight Generally, developers study performance-critical code carefully, and they write fastpaths to expedite important cases. Each such special case introduces more code that must be verified, with a corresponding increase in the required proof effort. Consequently, formal-methods researchers have introduced only those fastpaths necessary to get ‘good enough’ performance, stopping before achieving parity. In other words, verified code is not intrinsically slower, but verifying faster code can be more time consuming. It is also worth noting that it is impossible to achieve an ‘apples to apples’ performance comparison between verified and unverified systems, in that we cannot be sure that the unverified system is behaving correctly. At the limit, the unverified system could be doing the wrong thing very quickly.