Automated and Modular Refinement Reasoning for Concurrent Programs
This research explores automated modular refinement reasoning for concurrent programs, focusing on safety and correctness in operating systems and applications. Projects like Verve and Ironclad aim to achieve end-to-end security through formal verification tools and small trusted computing bases. The goal is to provide scalable automated verification methods, combining cryptography, secure hardware, and formal code verification to enhance system security.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
Automated and Modular Refinement Reasoning for Concurrent Programs Shaz Qadeer Collaborators: Chris Hawblitzel (Microsoft) Erez Petrank (Technion) Serdar Tasiran (Koc University)
Verve: a verifiably safe OS (Yang-Hawblitzel 10) Small Operating System (C#) every assembly language instruction checked for safety Verified Garbage Collector Verified Threads Verified Interrupt Handlers Verified Device Interface Verified Startup Verify safety & correctness with Boogie/Z3 Verified Boot x86 Hardware, Network, PCI, TPM 2 NDA. Microsoft Confidential.
An Ironclad app guarantees to remote parties that every instruction it executes adheres to a high-level security spec. I can run full SQL and the cloud learns nothing My password will never leak 3
Ironclad project (MSR OS Group) Goal: achieve end-to-end security Use small trusted computing base (TCB) thousands of lines of spec, not millions of lines of code Make approach feasible for use by system and application developers Show developers how to achieve correctness without testing Approach: Combine cryptography, secure hardware, and formal code verification Push scale of formal verification tools to fully encompass large systems 4
Ironclad apps atop Verve Notary Password Vault DiffPriv DB RSA Enc + Sig UDP/IP SHA Hash Big Integers Ethernet Bits & Arrays Math TPM Driver Net Driver Verified Garbage Collector Verified Threads Verified Interrupt Handlers Verified Device Interface Verified Startup Verified Boot x86 Hardware, Network, PCI, TPM 5 NDA. Microsoft Confidential.
Verve and concurrency Verve and concurrency Provides threads No mechanism to reason about them Difficult to provide any assurance beyond memory safety Verve boots on a single core Stop-the-world garbage collector Unacceptable multi-core performance
Goal of our work A scalable automated verifier for reasoning about low-level concurrency A verified concurrent garbage collector
Refining concurrent programs Verification works for me only when I start small. -Chris Hawblitzel Atomic actions as specifications Explicit non-interference (ala Owicki-Gries and Jones) Linear resources providing free invariants
Garbage collector implementation Extends Dijkstra et al. 78 multiple parallel mutators no read barrier fast write barrier Features Mark/Sweep/Idle phases separated by barriers Mutator cooperates with collector Barrier for atomic root scan
Garbage collector specification memAbs : [obj][fld]obj // Heap rootAbs : [idx]obj // Roots (stack, registers) allocSet: [obj]bool // Allocated objects
Garbage collector verification Simple high-level specification refined down individual instructions load, store, CAS, atomic increment/decrement Six levels of refinement 2100 lines of code and specification 6 min and 2GB memory on a modern Windows machine Simplifying assumptions Allocator is na ve (sequential search for free space) All objects have the same number of fields Sequentially consistent execution
Future work Verify under TSO Improve allocator performance Incorporate variable-size objects Extract executable code and plug into Verve
