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.
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.
2. Read This
|Reflections on Trusting Trust
ACM Turing Award lecture
Communications of the ACM 27(8):761–763, August 1984
Links: CACM article; Turing Award citation
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.
Links: AppGuarden home page; UK CyberSecurity Research Institute
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
|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.
SMACCMPilot: An Embedded Systems Software Research Project. Download the code and program your own impermeable quadcopter.