Parametric Verification of Address Space Separation Jason Franklin with Sagar Chaki, Anupam Datta, Jonathan M. McCune, Arvind Seshadri, and Amit Vasudevan Cylab & SEI @ Carnegie Mellon University 1 2 Parametricity Data structure reduction Refinement Verification of source code How we model adversaries Definition & Importance Interfaces Security Kernels

Outline Security Kernels Security kernels utilize protection mechanisms to prevent actions that violate a security policy APP Adversary OSes, hypervisors and web browsers Uses: cloud computing, online banking, DRM (PS3), malware testing, national security?, etc. Critically important to verify absence of security bugs Security Kernel Security Policy 3

State of the Art in Security Kernel Verification Manual/semi-automated verification Similar goals, costly and time consuming (requires patience) SRI HDM, InaJo, Gypsy, UCLA, PSOS, [Heitmeyer et al.], seL4 Model checking work for security kernels Study non-parametric verification [Guttman et al.], [Lie et al.], [Mitchell et al.] Bug finding with adversaries Unsound or incomplete methods [Kidd et al.], [Emmi et al.], [Bugrara and Aiken] 4 State of the Art in High-Assurance Systems App App App OS + TCB Hardware

App App App OS Hypervisor (TCB) Hardware Security-critical components extracted and moved to hypervisor Reduces system code size and interface < 10k L.O.C. and < 10 system calls Promising initial step to reduce complexity of verification TRANGO Virtual Processor, Open Kernel Labs OKL4, VirtualLogixs VLX, SecVisor (CMU), TrustVisor (CMU), and many others 5 Limitations of State of the Art Limitations Manual verification effort for theorem proving is high

Small TCBs alone dont enable automated formal verification Major source of complexity for model checking is size of data structures Our Goal Overcome limitations by exploiting structure of protection mechanisms 6 Approach Automatic source-level verification of OS protection mechanisms can be realized by: Parametrically reasoning about protection data structures and Using refinement to carry verification down to source code level 7 Verification Process Model system & property Apply Parametricity to reduce data structure size

Verification Source-level Verification Relate abstract models and C code Prove refinement & build refinement checker 8 Scope Systems Protection mechanisms of Xen, TrustVisor, SecVisor Manages protection data structures, performs permission and bounds checks

Properties Address separation, W xor X, access control Adversary model Adversary constrained to system interface 9 Outline Security Kernels How we model adversaries Interfaces Parametricity Refinement 10 Interface-Constrained Adversary Adversary model = arbitrary number of calls to system call interface with non-deterministic inputs Reduces complexity of adversary models, eases model checking Without Interface Abstraction

Interface-constrained Adversary Kernel Kernel Adversary A(w) A(*) B(x,y) B(*,*) C(z) C(*) 11 Example Adversary-Controlled Authoritative

* ReadWrite * eXe * Write Key Insights: Kernel page table is adversarycontrolled data structure Sync copies adversary-controlled data into memory Adversary is constrained to interface I = {Sync(*) , Add(*,*) , Delete(*)} Sync foreach row do if (Secure) then copy

Sys Call Interface Sync(*) Add(*,*) Delete(*) 12 Common Examples Remote Adversary Constrained to network interface Malicious Process Constrained to OS system call interface Malicious

Web Gadget Constrained to browser interface Adversary Malicious Periphera l Constrained to IOMMU interface 13 Outline Security Kernels Interfaces Data structure reduction Parametricity

Refinement 14 Protection Data Structures Kernel Page Table R Shadow Page Table UM RW UM W KD X KC WX

KC W UM=User Memory KD SecVisor Sync foreach row do if (W XOR X) then Sync KD=Kernel Data KC=Kernel Code 15 Data Structure Size and Verification Complexity Security kernels operate on large data structures Goal: automated verification Page tables, memory

protection structures, etc. techniques that scale gracefully Complexity of automated verification increases with increase in data structure size exponentially with increase in data structure size Page Table Entries States Space Time 3 55,000 8MB 4 1,700,000

5 -- Out of Memory -- 1024 -- -- -- <256MB 2 sec 360 sec Murphi model checking SecVisor security hypervisor with increasing page table size 16 Registers

cr3 Hierarchical Nesting Multi-level Page Tables PDT PT pde0 pte0 Memory Single-level Page Tables PT pte0 pte1 pde1 PT

pde2 pte0 pde3 pte1 pte2 17 Parametricity of System Data Structures shadow_paging_sync Row uniform foreach row do if (Row_Check) then modify row; n

Row independent 1 18 Small Model Analysis: Modeling Systems and Properties Model kernel and adversaries Parametric Guarded Command Language (PGCL) ADV(n) SYS(n) Apps Adversary SK(n) Security Kernel Express security properties Parametric Temporal

Specification Logic (PTSL) Policy P(n) 19 Language Design Challenges Balancing expressiveness with small model analysis Conditionals Whole array ops Assignment Parallel and sequential composition Non-deterministic update foreach row do if (Condition) then Set row = x; Adversary Distinctive features Modeling systems and adversaries: whole array operations

Adversary: Non-deterministic updates foreach row do row[0] = *; 20 Parametric Programming Language Language for modeling system & adversary Kernel Entry Finite number of Boolean variables System parameter: n Single parametric array: P of size n x q Parametric loop kernelmode ? kernelmode := ;; for i : Pn,q do Pn,q[i][Write] = T ? Pn,q[i][eXe] := ;; for i : P[n,q] do E ? C 21 SecVisor Model Sync

; ? for i : Pn,q do ; ? Pn,q[i][SPTPA] := Pn,q[i][KPTPA] Kernel Entry kernelmode ? kernelmode := ;; for i : Pn,q do Pn,q[i][SPTPA] = KC ? Pn,q[i][SPTRW] := ;; Pn,q[i][SPTX] := ;; Attacker ; ? for i : Pn,q do Pn,q[i][KPTPA] := ;; Pn,q[i][KPTRW] := ;; Pn,q[i][KPTX] := ; Kernel Page Table R UM R X KD

WX KC Shadow Page Table Sync R UM RW KD X KC 22 Expressive Specification Logic

Propositions Execution Integrity: Basic range over Booleans In kernel mode, only kernel Parametric range over rows of parameterized array code should be executable. It is stated as follows: Pexec == MODE=KERNEL( i P[i][eXe](P[i][CodeType] = KC))( i P[i][eXe](P[i][CodeType] = KC)) i P[i][eXe]( i P[i][eXe](P[i][CodeType] = KC))(P[i][CodeType] = KC)) Temporal logic specifications Reachability properties State formulas Universal, existential, and generic Path formulas Subset of ACTL* with USF as atomic propositions

23 Small Model Theorems Verify Sound: If small model is secure then large model is secure Complete: If small model is insecure then large model is insecure Insecure Secure! System(1) SMT Relate properties of System(1) to System(n), for all finite n Insecure Secure! System(n)

24 Small Model Safety Theorem System model Let gc(k) be any instantiated guarded command (i.e., any well-formed program) Security property Let in GSF be any generic state formula Forall i. P(i) , Exists i. P(i), or conjunctions of Initial state Let Init in USF be any universal state formula (For all i. P(i)) Definition: model exhibits if contains reachable state that satisfies Theorem: M(gc(k), Init) exhibits iff M(gc(1), Init) exhibits Thms with different initial conditions & properties in [Oakland2010] 25 Small Model Analysis Initial condition: SecVisor starts in kernel mode and only kernel code is executable SYS(n)

ADV(n) System Adversary In PTSL: mode = kernel AND Init == MODE=KERNEL FOREACH page in SPT, if^eXe then ( i P[i][eXe](P[i][CodeType] = KC)) i. P[i][SPTX] ( i P[i][eXe](P[i][CodeType] = KC))(P[i][SPTPA] = KC)) page maps kernel code RM(n) SecVisor(n) Execution Integrity:

In kernel mode, only kernel code should be executable. W xor X SMT Inmode PTSL: = kernel then If Pexec == MODE=KERNEL( i P[i][eXe](P[i][CodeType] = KC)) FOREACH page in SPT, if eXe then (page i P[i][eXe](P[i][CodeType] = KC)) i. P[i][SPTX] ( i P[i][eXe](P[i][CodeType] = KC))(P[i][SPTPA] = KC)) maps kernel code SecVisor(1) Verify 26 Verification Results

SecVisor (Shadowvisor, sHype, Xen), adversary, and properties expressible Small Model Theorems apply Translate to Murphi, verify Two vulnerabilities, repaired, verified Two more in ShadowVisor Sync ; ? for i : Pn,q do ; ? Pn,q[i][SPTPA] :=Pn,q[i][KPTPA] Secure Sync ; ? for i : Pn,q do ( Pn,q[i][SPTX] (Pn,q[i][KPTPA] = KC)) ? Pn,q[i][SPTPA] := Pn,q[i][KPTPA] 27 Extending Parametricity Results Complexities and Solutions page_fault (u32 addr) { pdt = get_pdt(addr);

Multiple, linked, parametric arrays if (pdt is ADDR) { if (pdt < MAX) copy; } else { if (getpde(addr) < MAX) copy; } Extended PGCL to handle multiple parametric arrays Added nested quantifiers to PTSL New small model theorems } 28 Related Work Parametric verification for correctness Missing whole array operators (adversary) or less efficient [Lazic et al.] and [Emerson and Kahlon] Incomplete methods (environment abstraction) [Clarke et al.] and [Talupur et al.]

Parametric verification for security Focus on security protocols [Lowe et al.], [Roscoe and Broadfoot], [Durgin et al.], [Millen] 29 Outline Security Kernels Interfaces Parametricity Verification of source code Refinement 30 Towards Source Level Verification Guarded Command Representation C code page_fault (u32 addr) { pdt = get_pdt(addr); if (pdt.ADDR) {

if (pdt < MAX) copy; } else { if (getpde(addr) < MAX) copy; } } Language containment refinement 1. Convert page_fault pdt.ADDR && pdt < MAX ? Pn,k[i][ADDR] := Pn,k[i] [ADDR]; !pdf.ADDR Refinement Theorem && pde(pdt) < MAX ? Pn,k[i][ADDR] := Pn,k[i] [ADDR];

2. Check language containment Yes, results apply. Convert C code to guarded commands (GC) Check language containment to prove GC is in PGCL No, modify or results do not apply. 31 Verification 1. Model system & property Verification

Apply Parametricity to reduce data structure size Relate abstract models and C code Prove refinement & build refinement checker Adversary abstraction to identify securityrelevant code Prove soundness & build abstractor 2. Source-level

Verification Complete In Progress 32 Expressiveness and Limitations PGCL/PTSL can model: Protection mechanisms that are row independent and row uniform Policies that are expressible as FSA over rows (safety properties) Developed compilation to convert FSA policy to PGCL reference monitor 33 Assumptions and/or Limitations Verification Applies to row-uniform, hierarchical-row independent systems (expressible in PGCL) Properties expressible in large subset of ACTL*/X Currently at model level and some source-level guarantees

Assumptions about semantics of C, correctness of model checker, translation tools, and of proofs Validation Security properties might not be right properties or strong enough Adversary model may not match reality 34 Related Work Model checking for security Study non-parametric verification of secure systems [Guttman et al.], [Lie et al.], [Mitchell et al.] Bug finding with adversaries Unsound or incomplete methods [Kidd et al.], [Emmi et al.] Operating system verification Manual/semi-automated verification [Walker et al.], [Heitmeyer et al.], [Klein et al.] 35 Questions?

Conclusions More info @ http://www.cs.cmu.edu/~jfrankli Towards scalable automated source-level verification of protection mechanisms Adversary abstraction reduces model complexity Parametric reasoning reduces data complexity Small model theorems relate small/large models Application to SecVisor, sHype, Shadowvisor, & Xen Refinement theorem pushes guarantees to source Outlined path to source level verification Building models is time-consuming, costly, and error-prone In progress, proof of refinement theorem 36