Transcript Modeling and Analysis of Networked Secure Systems

Modeling and Analysis of
Networked Secure Systems
with Application to Trusted
Computing
Jason Franklin
Joint work with Deepak Garg,
Dilsun Kaynar, and Anupam Datta
1
Motivation
•
Despite progress in cryptography and security
protocols, designing secure systems remains
difficult
–
Network protocols and cryptography rely on
secure system assumption
•
Problem: Attackers violate secure system
assumption by exploiting system design flaws
•
Solution: Prove security of system designs
2
Motivating Example
Client
System
Network
Server
System
3
Trusted Computing
• Question: How do we trust remote servers?
• Proposed Solution: Ask servers what
programs they are running?
– Server attests to (vouches for) its running software…
4
Details of Proposed Solution
System and Network Protocol
Analysis
Since I last
rebooted, I’ve
run
How
I’ll
Hey
I trust
ask
do
server!
Iwhat
know
those
0: Operating System
programs
ifWhat
programs
I cancode
trust
they
to
Network Protocol Analysis
1: Web Server
have
protect
that
have
you
server?
run!
my
run?
data!
2: Shopping Cart Server
Request
Client
System
Reply
Network
Server
System
5
In this talk…
• Describe Logic of Secure Systems (LS^2)
– Modeling system designs
– Analysis of system designs
• Analyze trusted computing protocol
• Limitations, work in progress, and conclusion
6
Modeling Protocols as Programs
Hey
I trust
server!
those
What
programs
code to
have
protect
youmy
run?
data!
Since I last rebooted, I’ve
run
0: Operating System
1: Web Server
2: Shopping Cart Server
request
Client
System
Reply
Network
Server
System
Client ≡
Server ≡
request := read question;
r := receive;
send request;
send reply;
reply := receive;
match /reply/trusted/;
7
Components of Model
Key:
Existing
Memory
Memory
Protection
Threads
Explicit
Time
Network
Comm.
Control
Flow
Hash
Hardware
Resets
Encryption
Decryption
Added
Trusted
Computing
Sign/Verify
8
Modeling Details
• Memory
– Read and write named memory locations
• Example: d := read Mem[x];
• Memory Protection
– Exclusive write locks
• Example: lock(Mem[x]);
• Explicit time
– Ordering events
• Read at time TR, Write at time TW and TR < TW
– Expressing invariants
• Mem[x] contains value V during interval (TR,TW)
9
New Adversary Model
I can generate
I can remove,
I’m a malicious local thread!
messages if I
reorder, or
know their
replay
I can write to any unprotected
components!
messages.
memory location!
I can read any memory location!
Client
System
Network
I collude with the network adversary!
Server
System
Standard Network Adversary
10
Overview of Protocol Analysis
Modeling
Analysis
Client ≡
request := read question;
send request;
reply := receive;
Suppose Client code
executed then:
Server is executing
trusted programs
match /reply/trusted/;
11
LS^2, what are you good for?
• Describe Logic of Secure Systems (LS^2)
• Analyze trusted computing protocol
• Limitations, work in progress, and
conclusion
12
Problems with Trusted Computing
Protocol
Hey
I trust
server!
those
What
programs
code to
have
protect
youmy
run?
data!
Since
Since II last
last rebooted,
rebooted, I’ve
I’ve
run
malicious
code.
run linux. Really, I have!
Mwhahaha!!!!
Reply
request
Client
System
Network
Malicious
Server
System
Client ≡
MALICIOUS_Server ≡
request := read question;
r := receive;
send request;
send “linux”;
reply := receive;
match /reply/trusted/;
13
Solution: Trusted Coprocessor
Trusted
Coprocessor
Client
System
Network
Server
System
14
Trusted Coprocessor
• Trusted Computing
– Augments platform with
trusted co-processor
Coprocessor
• Coprocessor includes:
– Crypto. Primitives
– Keys
– Append-only log
Log :
A
B
…
Log.append(A);
Log.append(B);
15
Server with Coprocessor
Server System
Booting ≡
1. append log, os_code;
Web Server
os := read os_code;
3. Append
4. Call
2. call os;
3. append log, web_server_code;
ws := read web_server_code;
OS
2. Call
4. call ws;
1. Append
Coprocessor
Log =
os_code
web_server_code
…
16
Coprocessor Vouching for Log
Signer ≡
_ := receive;
Log =
os_code
ws_code
…
w := read log;
s := sign w, K;
send s
s := SIGN K, (os_code, ws_code)
Client_Receive ≡
Client
System
verify s, seq(os_code, ws_code), K
s := receive;
17
Protocol Analysis
Modeling
Analysis
Client_Receive ≡
s := receive;
verify s, seq(os_code,
ws_code), K
Suppose Client code
executed then:
Server is executing
trusted programs
18
Trusted Computing Analysis
• Suppose that clients’s thread executes code
Client_Receive in time interval [Begin, End) then the
following properties hold:
Begin
End
No Resets during TR to TRead
19
Anyone See Security Vulnerability?
• Reset attack possible after read of log
Verification of
Stale Data
Client believes server
can be trusted!
Begin
End
No Resets during TR to TRead
Server
Reset
20
Adversaries Attack Assumptions
• Assumptions:
– Client is not running in coprocessor
– Coprocessor does not reveal its private key
– Coprocessor only executes Signer
– Programs in memory are write locked
21
Up next…
• Describe Logic of Secure Systems (LS^2)
– Designed for modeling and analysis of system
specifications
• Use LS^2 to analyze trusted computing
protocols
– Specify trusted computing protocols
– State security properties and security proof
– Discuss implications and analysis of proof
• Limitations, work in progress, and conclusion
22
Limitations and Work In Progress
• Control flow and context sensitive analysis
• Composition theorems for modular analysis of
complex systems
• Expanding access control policies
• Analysis of other trusted computing protocols
• Modeling layer diagrams
User Level Programs
Operating System
Hardware
23
Layer Diagram
Related Work
• LS^2 is derived from Protocol Composition
Logic [Datta05-07]
• Related work on program correctness:
– Concurrent separation logic [Brookes04]
– Verification of concurrent systems [TLA,
Lamport84, Owicki&Gries76]
24
Conclusion
• LS^2 is logic for analysis of networked secure
systems including local and network adversaries
• LS^2 models abstract memory protections, time,
hardware resets, and security primitives
• Described formal analysis of trusted computing
– Identified reset attack
• Ongoing work seeks to expand scope of LS^2
25
Take Home Points
• If you are designing secure systems:
– LS^2 enables security analysis of system
design before you implement
• Avoids costly and embarrassing vulnerabilities
• Clarifies security properties of design
• Even if you are just using secure systems:
– LS^2 can provide stronger guarantees about
your security
26
Questions?
• Theory of Secure Systems Project (ToSS)
– http://www.cs.cmu.edu/~jfrankli/toss
• Publications and Manuscripts:
– D. Garg, J. Franklin, D. Kaynar, A. Datta. “Towards a
Theory of Secure Systems” Cylab Technical Report,
Feb. 2008.
– D. Garg, J. Franklin, D. Kaynar, A. Datta. “A Logic for
Reasoning about Networked Secure Systems.” Under
submission to FCS ’08.
– J. Franklin, D. Garg, D. Kaynar, A. Datta. “Modeling
and Security Analysis of Trusted Computing.” In
progress.
27
2
28