Carnegie Mellon Secure Systems Verification Research
undefined
Limin Jia
Joint work with
Sagar Chaki, Anupam Datta, Jason
Franklin, Jonathan M. McCune and Amit Vasudevan
Software Model Checking
Secure Systems
A reference monitor
Mediating access to the hardware
Providing virtualization of the underlying hardware
Maximally privileged software
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
Hypervisors
Address Space Separation
Protection mechanisms
prevent execution contexts
from interfering w. each other
Separation achieved by
address translation subsystem
Guest
OS
Hypervisor
Automatically verify that separation mechanisms enforce
security properties in presence of adversary
Verification Task
Memory
OS
1
OS
2
Hypervisor
Hypervisor
Memory
Guest
Memory
Address Translation w. Page Tables
Virtual Address
i:
j:
k:
Scalability
Address translation data structures are complex due to size and
hierarchical nesting
Naïve use of model checker is unsuccessful
Challenges
Small Model Analysis
Is there structure in address translation subsystems that can
be exploited to improve scalability of model checking?
S
S’
R
Application of Small Model Analysis
P(n)
System
Adversary
Property
ADV(n)
SYS(n)
P(1)
System
Adversary
Property
ADV(1)
SYS(1)
Attack
Attack
Model checking
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
f
i
(x) = e
e is a PGCL+ expression
A canonical adversary
f
1
(*) | … |f
n
(*)
Small Model Analysis
P(1)
System
Adversary
Property
ADV(1)
SYS(1)
Attack
Specification Logic
Basic Proposition BP ::= b |
BP | BP
BP
Parametric Prop
PP(i
1
,…,i
z
) ::= A[i
1
]…[i
z
].f
bop
c
|
PP(i
1
,…,i
z
)
| PP(i
1
,…,i
z
)
PP(i
1
,…,i
z
)
U
n
i
v
e
r
s
a
l
F
o
r
m
U
S
F
:
:
=
B
P
|
i
1
,
…
,
i
z
,
P
P
(
i
1
,
…
,
i
z
)
|
B
P
i
1
,
…
,
i
z
,
P
P
(
i
1
,
…
,
i
z
)
E
x
i
s
t
e
n
t
i
a
l
F
o
r
m
E
S
F
:
:
=
B
P
|
X
i
1
,
…
,
X
i
z
,
P
P
(
i
1
,
…
,
i
z
)
|
B
P
X
i
1
,
…
,
i
z
,
P
P
(
i
1
,
…
,
i
z
)
G
e
n
e
r
a
l
F
o
r
m
G
S
F
:
:
=
U
S
F
|
E
S
F
|
U
S
F
E
S
F
LTL form F ::=
G
GSF |
F
GSF
PGCL++
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(*)
Example: ShadowVisor
ShadowVisor Vulnerability
Virtual Address
i:
j:
Adversary
Page
System
Code
Overlap
MEM_LIMIT
ShadowVisor Verification
•
Fixed separation check by adding page size to
conditional
•
Eliminates
page overlap vulnerability
•
Repaired system verified in less than 1 second
Proved the soundness of the small model analysis
Performed case studies of several hypervisors
Results [Oakland S&P11, Post12]
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
Ongoing and Future Work
End-to-end Verification
P(n)
System
Adversary
Property
ADV(n)
SYS(n)
P(1)
System
Adversary
Property
ADV(1)
SYS(1)
Attack
Attack
Model checking
End-to-end Verification
C
Implementation
Abstract
Model (n)
Abstract
Model (1)
Identify interfaces
Prune irrelevant code
Refinement between C code and PGCL++ abstraction
Memory safety of the C implementation is crucial
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.]
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
