Transcript PPT - Formal Reasoning Group

Composable Formal Models
for
High-Assurance Fault
Tolerant Networks
Carolyn Talcott
SRI International
FTN PI meeting January 2003
People
• PIs:
• Carolyn Talcott (SRI)
• Jose Meseguer (UIUC)
•
•
•
•
03Jan27
Other team members:
Steven Eker (SRI)
Mark-Oliver Stehr (UIUC)
Ambarish Sridharanarayanan (UIUC)
2
Composable Formal Models
for High-Assurance Fault Tolerant Networks
New Ideas



S 
Libraries of formal models of attacks
Formal executable framework for
reflective systems
Formal test bed for design of network
reconstitution and recovery services
model
checking
rapid
prototyping
state space
search
Impact
•
•
•
03Jan27
Sound principles for composition of network
reconstitution and recovery services
Higher assurance for FTN protocols and algorithms
Compliment red team efforts to harden systems
Schedule
07/02
Task 1:
Case Studies
07/03
C1
Task 2:
Framework
Mobile Maude
SRI International: Carolyn Talcott
University of Illinois Urbana-Champaign: José Meseguer
3
Some Possible Case Studies
 Proxy-based Distributed Systems
– secure distribution of component based systems
• DDOS models
– formal attack models, formal v&v?
• Secure Spread (Maude + uCAPSL)
– is it secure?
– is the group semantics preserved?

TIARA project
– intrusion tolerance for ad hoc networks
• Distributed/replicated databases
03Jan27
– formal verification of core algorithms
– reuse to verify DB specific optimizations
4
Analysis of
Secure Proxy Toolkit
In collaboration with DC project
Securing Proxy-based Distributed Systems
John Mitchell, Ninghui Li, Derrick Tong
Stanford
03Jan27
5
Proxy based distributed service
End2end view
RegistryNode
Reg: db
Register
LookUp
ServerNode
ClientNode
findSvc
App
SvcCall
03Jan27
sTk
cTk
cPxy
Remote Messaging
Register
SvcMgr
SvcCall
sPxy
Svc
6
Security Goals
• Client VM protected from evil proxy
• Secure communication between client and server
proxies
• Client should be able to authenticate service proxy
• Server should be able to authenticate client
03Jan27
7
The Secure Proxy Toolkit
in
Pictures
03Jan27
8
Registering a signed secure proxy
ServerNode
RegistryNode
Reg: db
4
3
sTk
1. RegReq(svcName,Svc)
2. create(sAP)
3. sign(cAPd)
4. register(svcName,signedcAPd)
sTms
SvcMgr
1
2
Svc
sAP
ServerNode
RegistryNode
Reg: db’
sTk
sTms
SvcMgr
sAP
Svc
03Jan27
9
Getting an authentication proxy
RegistryNode
ClientNode
2
App
1
cSTm
4
Reg: db’
3
cTk
ServerNode:S
5
5a
cAP
sTk
sSTs
sAP
Svc
1. findSvc(svcName)
2. lookup(svcName)
3. reply(signedcAPd)
4. verify(signedcAPd,tsK)
5. ok(apxd)
5a. install(apxd)
03Jan27
 must check description!
10
Setting up a secure session
ClientNode
App
cSTm
17
14
15
ServerNode:S
sSTm
cTk
sTk
6
7
cAP
9
12
Svc
10
16
6. authenticate(ccred)
6a. setup secure cnx --7. authenticate(ccred)
8. checkClient(ccred,svcName)
9. clientOk(perms)
10. install(sspd)
03Jan27
11
sAP
13
cSP
8
sSP
11. encryptReq(csspd,ccred)
12. encrypted(csspd,ccred)
13. encrypted(csspd,ccred)
14. decrypt(encrypted(csspd,ccred))
15. ok(csspd)
16. install(csspd)
17. findSvcReply(cSP)
11
Accessing the service
ClientNode
App
ServerNode:S
cTk
sSTm
sTk
16
cSTm
21
cAP
sAP
18
17
sSP
cSP
Svc
19
20
16. serviceCall(args)
17. serviceCall(args)
18a. check(args,per)
18. serviceCall(args,cId)
03Jan27
19. serviceReply(result)
20. serviceReply(result)
21. serviceReply(result)
12
Proxy Toolkit Models
4 levels of security
• Level 0 -- naive proxy (just does rmi)
• Level 1. naive proxy enhanced with secure
communication
• Level 2[t,f]. signed proxy
– [with,without] checking proxy service name
• Level 3. signed proxy with authentication
(and secure session)
03Jan27
13
Registering a service
Levels 0,1
SvcMgr
Levels 2,3
sPTK0
Lup
spRegister
SvcMgr
TMS
sPTK0
spRegister
create
create
sSP
registerReq
signReq
sSP/sAP
signReply
registerReq
registerReply
registerReply
Lup
registerReply
registerReply
Levels differ in choice of proxy behavior
03Jan27
14
Scenario -- finding and using a service via Level 0,1 PTK
App
sSP
cSPTk
Svc
findService
Lup
lookUp
secProxy
install
findServiceReply
Attack Proxy Installedl
cSP
SvcCall
SvcCall
SvcCall
access to client data
SvcReply
SvcReply
SvcReply
clear in level 0, secure in level 1
03Jan27
Illegal Call
point of attack
15
Scenario -- finding and using a service via Level 2 PTK
App
cTMS
sSP
cSPTk
sTMS
Svc
findService
Lup
lookUp
verify
signedProxy
ok
check descr?
install
findServiceReply
cSP
Proxy to wrong service
if no check
SvcCall
SvcCall
SvcCall
SvcReply
SvcReply
SvcReply
03Jan27
Illegal Call
16
Scenario -- finding and using a service via Level 3 PTK
App
cTMS
sAP
cSPTk
findService
Svc
Lup
lookUp
verify
ok
sTMS
signedProxy
check descr
install
cAP
authenticate
authenticate
encrypted cSP
decrypt
create
ok
install
findServiceReply
SvcCall
cSP
sSP
SvcCall
check
SvcReply
03Jan27
SvcReply
ckClient
ok
SvcCall
SvcReply
17
Attack Model I
1. Attacker in the ether + independent imposter
Properties checked:
• 1.1 attacker see/modify client data
– sent as service arguments or received as reply
• 1.2 attacker replace registered proxy
• 1.3 illegal or unauthorized service call
• 1.4 client imposter succeeds
03Jan27
18
Summary of analyses
attacker in net
Level 0
1.1
msg
attack
yes
1.2
replace
proxy
yes
1.3
illegal
call
yes
1.4
imposter
succeeds
yes
Level 1
no
yes
yes
yes
Level 2f
no
yes
yes
yes
Level 2t
no
no
yes
yes
Level 3
no
no
no
no
Property:
yes/no Property holds/not
03Jan27
19
Attack Model II
2. Attacker controls Lookup node
Properties checked:
• 2.1 client app can get proxy to requested/registered
service (sanity check)
• 2.2 client app accepts proxy to attacker service
• 2.3 client app accepts wrong proxy
• 2.4 service integrity violated
03Jan27
20
Summary of analyses
compromised registry
Property:
2.2
bad
proxy
yes
2.3
wrong
proxy
yes
2.4
impersonate
Level 0
2.1
sanity
check
yes
Level 1
yes
yes
yes
yes
Level 2f
yes
no
yes
yes
Level 2t
yes
no
no
yes
Level 3
yes
no
no
no
yes
yes/no Property holds/not
03Jan27
21
What Next

TIARA intrusion tolerance for ad hoc networks


abstract router and network model
composing - router, TIARA, TCP/IP layer
• DDOS models (JHU/APL)
– attacks with classification mitigagtion technology
– TCP SYN flood attack / Synkill active monitoring

Secure Spread (Maude + uCAPSL)
– abstract spread network model
– compose with Cliques model
03Jan27
22