Automated and Modular Refinement Reasoning for Concurrent Programs
Automated and Modular Refinement Reasoning
for Concurrent Programs
Collaborators:
Chris Hawblitzel (Microsoft)
Erez Petrank (Technion)
Serdar Tasiran (Koc University)
Shaz Qadeer
2
Small Operating System
(C#)
Verify
safety &
correctness
with
Boogie/Z3
“every assembly
language instruction
checked for safety”
Verve: a verifiably safe OS (Yang-Hawblitzel 10)
An
Ironclad app
guarantees
to remote parties
that
every instruction
it executes adheres to a
high-level security
spec
.
3
My password will never leak
I can run full SQL and the
cloud learns nothing
•
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 project (MSR OS Group)
Ironclad apps atop Verve
5
V
e
r
v
e
a
n
d
c
o
n
c
u
r
r
e
n
c
y
•
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
•
Atomic actions as specifications
•
Explicit non-interference (ala Owicki-Gries and Jones)
•
Linear resources providing free invariants
Verification works for me only when I start small.
-Chris Hawblitzel
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
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.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
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.
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
