Carnegie Mellon Secure Systems Verification Research
Carnegie Mellon University's research focuses on secure hypervisor systems, address space separation, and verification tasks to ensure security properties in the presence of adversaries. Challenges include scalability in model checking due to complex data structures in address translation. The aim is to exploit the structure of address translation subsystems for improved scalability.
Uploaded on Sep 06, 2024 | 3 Views
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
Carnegie Mellon Software Model Checking Secure Systems Limin Jia Joint work with Sagar Chaki, Anupam Datta, Jason Franklin, Jonathan M. McCune and Amit Vasudevan
Carnegie Mellon Hypervisors A reference monitor Mediating access to the hardware Providing virtualization of the underlying hardware Ensure that the hypervisor implementation has desired security properties Maximally privileged software Address space separation property Direct access to hardware Maintains guest operating system states The security of the entire system depends critically on whether the hypervisor correctly enforces the desired security policies 2
Carnegie Mellon Address Space Separation Protection mechanisms prevent execution contexts from interfering w. each other Guest OS Separation achieved by address translation subsystem Hypervisor Safe Memory Unsafe Memory A B A B 3
Carnegie Mellon Verification Task Automatically verify that separation mechanisms enforce security properties in presence of adversary OS1 OS2 Guest virtual addresses are never mapped to hypervisor memory Hypervisor Memory Hypervisor Memory Guest Memory 4
Carnegie Mellon Address Translation w. Page Tables Virtual Address i j k o Memory Pages k: j: i: Guest OS Data System Code 5
Carnegie Mellon Challenges Scalability Address translation data structures are complex due to size and hierarchical nesting Na ve use of model checker is unsuccessful Page Table Size Time (seconds) Variables Clauses 1 <1 1k 3k 10 3 93k 199k 20 >35 360k 775k 30 Out of Mem Out of Mem Out of Mem 6
Carnegie Mellon Small Model Analysis Is there structure in address translation subsystems that can be exploited to improve scalability of model checking? Row independent 7
Carnegie Mellon S R S 8
Carnegie Mellon Application of Small Model Analysis Model checking ADV(n) ADV(1) Adversary Adversary Attack Attack System System SYS(n) SYS(1) Property Property P(n) P(1) 9
Carnegie Mellon Small Model Analysis Express security properties Parametric Temporal Specification Logic (PTSL+) Model system and adversaries Parametric Guarded Command Language (PGCL+) Row-independent nested array accesses Adversaries Bounded by interfaces fi(x) = e e is a PGCL+ expression A canonical adversary f1(*) | |fn(*) ADV(1) Adversary Attack System SYS(1) Property P(1) 10
Carnegie Mellon Specification Logic Basic Proposition BP ::= b | BP | BP BP Parametric Prop PP(i1, ,iz) ::= A[i1] [iz].f bop c | PP(i1, ,iz) | PP(i1, ,iz) PP(i1, ,iz) Universal Form USF ::= BP | i1, ,iz,PP(i1, ,iz) | BP i1, ,iz,PP(i1, ,iz) Existential Form ESF ::= BP | Xi1, ,Xiz,PP(i1, ,iz) | BP Xi1, ,iz,PP(i1, ,iz) General Form GSF ::= USF | ESF | USF ESF LTL form F ::= GGSF | F GSF 11
Carnegie Mellon PGCL++ 12
Carnegie Mellon Example: ShadowVisor Properties: No physical address above MEMLIMIT is accessible by adversary Psep == i1,i2 . (P[i1].F[PRESENT] (P[i1].F[ADDR] < MEMLIMIT)) AND (P[i1].P[i2].F[PRESENT] (P[i1].P[i2].F[ADDR] < MEMLIMT)) Interfaces: shadow_new_context( ) shadow_page_fault(*) shadow_page_invalidate(*) 13
Carnegie Mellon ShadowVisor Vulnerability Virtual Address i j o Memory j: i: Adversary Page Overlap MEM_LIMIT System Code 14
Carnegie Mellon ShadowVisor Verification Page Table Size Time (seconds) Variables Claues 1 <1 3 1k 93k 3k 10 199k 20 >35 360k 775k 30 Out of Memory Out of Memory Out of Memory Fixed separation check by adding page size to conditional Eliminates page overlap vulnerability Repaired system verified in less than 1 second 15
Carnegie Mellon Results [Oakland S&P11, Post12] Proved the soundness of the small model analysis Performed case studies of several hypervisors 16
Carnegie Mellon Ongoing and Future Work Making PGCL+ more expressive Accesses include both loop and selection of one row End-to-end sound verification Relating C program to abstract PGCL++ model Other security Properties 17
Carnegie Mellon End-to-end Verification Model checking ADV(n) ADV(1) Adversary Adversary Attack Attack System System SYS(n) SYS(1) Property Property P(n) P(1) 18
Carnegie Mellon End-to-end Verification C Abstract Model (n) Abstract Model (1) Implementation Identify interfaces Prune irrelevant code Refinement between C code and PGCL++ abstraction Memory safety of the C implementation is crucial 19
Carnegie Mellon 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.] 20
