This afternoon’s lecture presented ways to take proofs of code properties beyond correctness or safety of specific code into the domain of mobile applications, guarantees of trustworthiness, and complete systems.
It’s now standard to use digital certificates to authenticate software, providing information about where it comes from. However, this doesn’t actually say anything about the code itself. The technique of Proof-Carrying Code complements authentication with digital evidence that affirms specific properties of the code. These guarantees can be independently checked and are robust under malicious modification of any component.
Even with verified source code, its eventual behaviour still depends on compilers, libraries, operating systems, hardware, and more: all of these are areas of current research into verification and correctness, with some success but still considerable challenge.
Homework
1. Do This
Watch this ten-minute video where Kathleen Fisher, HACMS project leader, explains the background to the proposed research. If you would like to find out more then follow the references at the end of this post.
Link: Dr Fisher introducing HACMS
2. Read This
 |
Reflections on Trusting Trust Ken Thompson ACM Turing Award lecture Communications of the ACM 27(8):761–763, August 1984 Links: CACM article; Turing Award citation |
References
Digital Certificate Failure Modes
Three noted failures of digital certificates to authenticate code. Two of these were malicious subversion, but the shipping of a virus within a Microsoft product appears to have been accidental and shows a characteristic gap within digital certification: it is only the provider that is being certified, not the contents of the code.
 |
Microsoft Security Bulletin MS01-017 – Critical Erroneous VeriSign-Issued Digital Certificates Pose Spoofing Hazard Attacker could digitally sign code using the name “Microsoft Corporation” Link: Full text of bulletin |
 |
Microsoft Inadvertently Ships Nimda Virus in Visual Studio .NET As reported in Windows IT Pro, June 2002 File containing the virus was distributed in the Korean version of VS.NET. Links: News article; Article from Microsoft |
 |
Microsoft throws ‘kill switch’ on own certificates after Flame hijack As reported in Computerworld, June 2012 Microsoft revoked certification authority subverted by the Flame malware. Links: News article; Microsoft security advisory |
Edinburgh Research on Mobile Code Security
 |
Mobile Resource Guarantees Proof-carrying code that certifies Java app performance Edinburgh / Munich collaboration 2002–2005 Links: Summary leaflet; MRG home page |
 |
Mobius: Mobility, Ubiquity and Security Enabling proof-carrying code for Java on mobile devices. European integrated project 2004–2009 Links: Slides; Poster; Mobius home page. |
 |
AppGuarden: Resilient Application Stores Enhancing App Stores with fine-grained policies discovered through machine learning and enforced using machine-checkable digital evidence. Edinburgh 2013–2016 Links: AppGuarden home page; UK CyberSecurity Research Institute |
Compiler Verification
 |
CompCert The CompCert C verified compiler comes with a mathematical, machine-checked proof that the generated executable code behaves exactly as prescribed by the semantics of the source program. Link: CompCert home page |
 |
Cerco: Certified Complexity Verified execution costs for an embedded microcontroller. Edinburgh / Bologna / Paris collaboration 2010–2013 Link: CerCo home page |
 |
CompCertTSO: A Verified Compiler for Relaxed-Memory Concurrency Compiles C to x86, verified against the Total Store Order concurrency model. Link: CompCertTSO home page |
Platform Verification
 |
SAFE: A Secure Computing Platform Tagged hardware architecture for flexible security checking. Part of DARPA CRASH: Clean-slate design of Resilient, Adaptive, Secure Hosts. Links: SAFE home page; DARPA CRASH programme |
 |
seL4: A Secure OS Kernel Verified implementation of the L4 operating system microkernel. National ICT Australia (NICTA) Link: seL4 home page |
 |
REMS: Rigorous Engineering for Mainstream Systems Verification of CPU architectures, systems code, concurrent software. Cambridge / London / Edinburgh 2013–2019 Link: REMS home page |
HACMS: High-Assurance Cyber-Military Systems
Verified security for embedded control systems and autonomous vehicles. Uses automated code synthesis, embedded Haskell DSLs for realtime hardware control, and machine-checked safety proofs.
-
DARPA Unveils Hack-Proof Drone. Defense Tech, May 2014.
Ignore the lead photograph: there’s a more sensible one of the quadcopter further down. -
Pentagon on Path to Launch Hacker-Proof Boeing Drone by 2018. Nextgov, March 2015.
The source code for the quadcopter is available online, and it was the subject of a couple of talks at IFCP 2014, the annual International Conference on Functional Programming.
-
Using Formal Methods to Enable More Secure Vehicles: DARPA’s HACMS Program. Kathleen Fisher, ICFP keynote address, September 2014.
DOI: 10.1145/2692915.2628165 -
Building embedded systems with embedded DSLs. Hickey et al., September 2014
DOI: 10.1145/2692915.2628146 — Video -
SMACCMPilot: An Embedded Systems Software Research Project. Download the code and program your own impermeable quadcopter.
http://www.smaccmpilot.org