Lecture 14: Certifying Correctness

Title slideThis 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.

Links: Slides; Recording

Homework

1. Do This

Video frameWatch 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
Final step in Ken Thompson's trojan program from his Reflections on Trusting Trust 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.

Screenshot 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
Screenshot 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
 Screenshot 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
MRG logo Mobile Resource Guarantees
Proof-carrying code that certifies Java app performance
Edinburgh / Munich collaboration 2002–2005
Links: Summary leaflet; MRG home page
Mobius logo 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 image 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 chain 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
Photo of SAFE enclosure 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 logo seL4: A Secure OS Kernel
Verified implementation of the L4 operating system microkernel.
National ICT Australia (NICTA)
Link: seL4 home page
REMS logo 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.

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.2628146Video

  • SMACCMPilot: An Embedded Systems Software Research Project. Download the code and program your own impermeable quadcopter.
    http://www.smaccmpilot.org