Ensuring End-to-End Security in Low-Level Code
Formally prove an information flow policy for low-level code systems, dealing with challenges in C and assembly languages, compilation, security preservation, and declassification. Explore a new methodology for specifying, proving, and propagating security policies, with application to a verified OS kernel.
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
David Costanzo Yale University David Costanzo, Zhong Shao, Ronghui Gu PLDI 2016 June 17, 2016
Goal Goal: formally prove an end-to-end information-flow policy that applies to the low-level code of these systems VM 1 VM 2 Proc 1 Proc 2 Hypervisor OS Kernel Mach 1 Mach 2 a.com b.com Distributed System Web Browser
How to specify the information flow policy? ideally, specify at high level of abstraction allow for some well-specified flows (e.g., declassification) Proc 1 Proc 2 policy? policy? OS Kernel
Most systems are written in both C and assembly must deal with low-level assembly code must deal with compilation even verified compilation may not preserve security
How to prove security on low-level code? Security type systems (e.g., JIF) don t work well for weakly- typed languages like C and assembly How do we deal with declassification? Systems may have internal leaks hidden from clients How to prove security for all components in a unified way that allows us to link everything together into a system-wide guarantee?
New methodology to specify, prove, and propagate IFC policies with a single unifying mechanism: the observation function specify expressive generalization of classical noninterference prove general proof method that subsumes both security label proofs and information hiding proofs propagate security-preserving simulations
Application to a real OS kernel (CertiKOS [POPL15]) First fully-verified secure kernel involving C and assembly, including compilation Verification done entirely within Coq Fixed multiple bugs (security leaks) Policy influence each other in any way (IPC disabled) Policy: user processes running over CertiKOS cannot
Observation Function Security Policy Proof: spec secure wrt policy Verified Security- Preserving Simulation End-to-End Guarantee x86 Machine Model
1. Specifying security 2. Proving security (example) 3. Propagating security across simulations 4. Experience with CertiKOS security proof
Alices behavior is influenced only by her own data. Bob Alice Bob1 1 Alice Bob Alice Bob1 1' ' Alice' ' = = Bob Alice Bob2 2 Alice Bob Alice Bob2 2' ' Alice' '
Alices behavior is influenced only by her own observation. 1 1 1 1' ' A A( ( 1 1) ) A A( ( 1 1' ) ' ) = = 2 2' ' 2 2 A A( ( 2 2' ) ' ) A A( ( 2 2) )
: : principal program state observation (can be any type) S S : : program state program state prop spec S is secure for principal p 1 1 , , 2, 2, 1, 1, 2 2 . . p p( ( 1 1) = ) = p p( ( 2 2) ) S( 1, p p( ( 1 1) = 1, 1 1) ) S( 2, 2, 2 2) ) ) = p p( ( 2 2) )
A A w x y z (5, {A}) (17, {A,B}) (42, {B}) (13, {}) w x y z (5, {A}) (?, {A,B}) (?, {B}) (13, {}) {A,B} {A} A A {B} {}
A A employee salaries avg salary Bob s detailed event calendar Bob s available / unavailable time slots M M T T W W F F M M T T W W F F A A
1. Specifying security 2. Proving security (example) 3. Propagating security across simulations 4. Experience with CertiKOS security proof
va_load va_load Process p Process p va p( ) := fun va => va_load va global heap pa data page tables Definition va_load va rs rd := match ZMap.get (PDX va) (ptpool ) with PDEValid _ pte => match ZMap.get (PTX va) pte with | PTEValid pg _ => Next (rs # rd <- FlatMem.load (HP ) (pg*PGSIZE + va%PGSIZE)) | PTEUnPresent => exec_pagefault va rs end end. Declassify? High Security
1. Specifying security 2. Proving security (examples) 3. Propagating security across simulations 4. Experience with CertiKOS security proof
OS and compiler refinement proofs use simulations Simulations may not preserve security! swap(x,y) x y 17 42 x y 42 17 Machine M Machine M R R z = x; x = y; y = z x y z 42 17 17 x y z 17 42 0 Machine N Machine N ? ??,?? (??? = ??? ??? = ??(?))
Define an observation function for each Require that the simulation is security-preserving each machine, M and N Security Security- -Preserving Simulation Preserving Simulation (for principal p) 1 1 , , 2, 2, s s1, 1, s s2 2 . . M Mp p ( ( 1 1) = ) = M Mp p ( ( 2 2) ) R( 1, ) = N Np 1,s s1 1) ) R( 2, 2,s s2 2) ) N Np p (s (s1 1) = p (s (s2 2) ) No significant changes to CompCert were needed
1. Specifying security 2. Proving security (examples) 3. Propagating security across simulations 4. Experience with CertiKOS security proof
Certified functionally correct OS kernel with 32 layers 354 lines of assembly code, ~3000 lines of C code CompCert compiles C to assembly Each layer has primitives that can be called atomically Bottom layer MBoot is the x86 machine model Top layer TSysCall contains 9 system calls as primitives init, vmem load/store, page fault, memory quota, spawn child, yield, print
For a process p, the observation function is: registers, if p is currently executing the output buffer of p the function p s available memory remaining (quota) the number of children p has spawned the saved register context of p the spawned status and currently-executing status of p function from p s virtual addresses to values
Sp = (as described) TSysCall R Ip= p s current output buffer p s final output buffer (whole-execution behavior) MBoot BIp = Generalized Noninterference: Generalized Noninterference ,?2 ? ?2,?2 = ? . ?1,?2,?1 ??2 ?1,?1 ? ? ??1 = ? ? ) ??1 ?(?2 End End- -to to- -End Security End Security: ?1,?2,?1,?2 . ??2 ?1,?1 ? ?2,?2 ? ?? ? ??1 = ? ??1 = ?? ?(?2)
function bob { int secret = 42; for i = 0 to secret { proc_spawn(); } yield(); } function alice { int pid1 = proc_spawn(); yield(); int pid2 = proc_spawn(); print(pid2 pid1 + 1); } || IDs pid1 pid2 secret
max children = 3 0 0 1 1 2 2 3 3 5 5 4 4 6 6 8 8 7 7 9 9 11 11 10 10 12 12
New methodology using observation function to specify, prove, and propagate IFC policies applicable to all kinds of real-world systems! Verification of secure kernel done fully within Coq machine-checked proofs! Future Work realistic x86 model, preemption, concurrency Future Work: virtualized time (already done), more
CertiKOS info - http://flint.cs.yale.edu/certikos/ PLDI certified artifact - ask me for link
