4.7 KiB
Executable File
| readstatus | dateread | title | year | authors | citekey | journal | volume | issue | pages | ||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| false | Formally verified software in the real world | 2018 |
|
kleinFormallyVerifiedSoftware2018 | Commun. ACM | 61 | 10 | 68–77 |
Indexing Information
DOI
ISBN
Tags:
#formal-verification, #Control-systems, #Cybersecurity, #penetration-testing, #Formal-methods
[!Abstract] Verified software secures the Unmanned Little Bird autonomous helicopter against mid-flight cyber attacks.
[!note] Markdown Notes None!
Annotations
[!attention] Highlight key insights ˽ Formal proof based on micro-kernelenforced software architecture can scale to real systems at low cost. ˽ Mixed assurance levels and security levels within one system are possible and desirable; not all code has to be assured to the highest level. ˽ High assurance can be retrofitted to suitable existing systems with only moderate redesign and refactoring.
[!done] Quote Its foundation is our verified microkernel, seL4, discussed later, which guarantees isolation between subsystems except for well-defined communication channels that are subject to the system’s security policy.
[!attention] Highlight Note we primarily use formal verification to provide proofs about correctness of code that a system’s safety or security relies on. But it has other benefits as well. For example, code correctness proofs make assumptions about the context in which the code is run (such as behavior of hardware and configuration of software). Since formal verification makes these assumptions explicit, developer effort can focus on ensuring the assumptions hold—through other means of verification like testing. Moreover, in many cases systems consist of a combination of verified and non-verified code, and in them, formal verification acts as a lens, focusing review, testing, and debugging on the system’s critical nonverified code.
[!done] Quote The mechanisms support its use as a hypervisor to, say, host entire Linux operating systems while keeping them isolated from security-critical components that might run alongside, as outlined in Figure 1. In particular, this functionality allows system designers to deploy legacy components that may have latent vulnerabilities alongside highly trustworthy components.
[!attention] Highlight The dual of integrity is confidentiality, which states that a component cannot read another component’s data without permission,2
[!note] Note Integrity: The inability for process A to mess with process B unless explicitly defined as being allowed to.
Confidentiality: Process A cannot READ anything that it isn't explicitly allowed to
[!attention] Highlight the link between Linux and the crypto component in Figure 4 is for message passing only and does not give access to memory. Only authenticated messages can reach the CAN bus, as the crypto component is the only connection to the driver. Untrusted payload software and WiFi are, as part of the Linux VM, encapsulated by component isolation and can communicate to the rest of the system only via the trusted crypto component.
[!question] Don't Understand The mechanisms of the seL4 kernel discussed earlier can achieve this enforcement, but the level of abstraction of the mechanisms is in stark contrast to the boxes and arrows of an architecture diagram; even the more abstract access-control policy still contains far more detail than the architecture diagram. A running system of this size contains tens of thousands of kernel objects and capabilities that are created programmatically, and errors in configuration could lead to security violations. We next discuss how we not only automate the configuration and construction of such code but also how we can automatically prove that architecture boundaries are enforced.
[!done] Quote Due to the isolation provided by seL4 and the componentized architecture, it becomes possible for components of mixed assurance levels to coexist in the system without decreasing the overall assurance to that of the lowest-assurance component or increasing the verification burden of the lowest-assurance components to that of the highest-assurance ones.
[!attention] Highlight The right granularity is a trade-off between the strength of isolation on the one hand and the increased overhead and cost of communication between partitions, as well as re-engineering cost, on the other.