Loading presentation...
Prezi is an interactive zooming presentation

Present Remotely

Send the link below via email or IM

Copy

Present to your audience

Start remote presentation

  • Invited audience members will follow you as you navigate and present
  • People invited to a presentation do not need a Prezi account
  • This link expires 10 minutes after you close the presentation
  • A maximum of 30 users can follow your presentation
  • Learn more about this feature in our knowledge base article

Do you really want to delete this prezi?

Neither you, nor the coeditors you shared it with will be able to recover it again.

DeleteCancel

Make your likes visible on Facebook?

Connect your Facebook account to Prezi and let your likes appear on your timeline.
You can change this under Settings & Account at any time.

No, thanks

Formal Verification of a Tiny Separation Kernel

SICS Security Seminar 2014
by

Oliver Schwarz

on 23 September 2016

Comments (0)

Please log in to add your comment.

Report abuse

Transcript of Formal Verification of a Tiny Separation Kernel

ARM v7
Hypervisor
guest 1
system to be verified
MMU
message handler
guest 2
message handler
buffer
release
send
H
igh
O
rder
L
ogic
B
inary
A
nalysis
P
latform
{pre} code {post}
check
lift binary
compute weakest precondition
check pre(v) wp (code, post(v)) for all bitvectors v
[using SAT solver]
discover counterexample
interactive theorem prover
open source
based on Standard ML
Cambridge ARM model
(monadic operational semantics)
enhanced by MMU
ARM v7
guest 1
specification
message handler
guest 2
message handler
buffer
ARM v7
bisimulation
mem [ P | Am | Im ]
reg [ Ar | Ir ]
...
mem [ P | Am' | Im ]
reg [ Ar' | Ir ]
...
Non-Exfiltration
mem [ P | Am' | . ]
reg [ Ar' | . ]
...
Non-Infiltration
mem [ P | Am | . ]
reg [ Ar | . ]
...
mem [ P | Am | . ]
reg [ Ar | . ]
...
mem [ P | Am' | . ]
reg [ Ar' | . ]
...
Security during user
mode execution
more: timing
more: functionality
Formal Verification of a Tiny Separation Kernel
speaker: Oliver Schwarz
"Encryption works. Properly implemented strong crypto systems are one of the few things that you can rely on.
Unfortunately, endpoint security is so terrifically weak that NSA can frequently find ways around it.
"
-- Edward Snowden

ARM v7
Separation Kernel
paravirtualized
(without virtualization support)
John Rushby
Partitions should be physically indistinguishable from distributed systems.
(1981)
prosper.sics.se
Formal Verification of Information Flow Security for a Simple ARM-Based Separation Kernel
Mads Dam, Roberto Guanciale, Narges Khakpour, Hamed Nemati and Oliver Schwarz
ACM Conference on Computer & Communications Security (CCS'13).
Machine Assisted Proof of ARMv7 Instruction Level Isolation Properties
Narges Khakpour, Oliver Schwarz and Mads Dam
Certified Programs and proofs (CPP'13).
Machine Code Verification of a Tiny ARM Hypervisor
Mads Dam, Roberto Guanciale, Hamed Nemati
TrustED 2013.
Read about it ...
boot
mode switch
user mode
handlers
bugs found
restoring of control flags
determining last guest instruction
lifter
Mads Dam
Roberto Guanciale
Hamed Nemati
Narges Khakpour
Arash Vahidi
Christian
Gehrmann
Viktor Do
every difference leaks
access control
clean up
hide your management data
angry boys
angry teacher
no class
relaxed
teacher
non-interference
lucky girls
angry boys
angry teacher
suffering
girls
no class
relaxed
teacher
lucky girls
interference
relaxed
teacher
relaxed
teacher
break
lucky girls
remember the tactic of delaying the teacher?
run Linux with dynamic memory management
more: devices
DMA devices in a context of secure virtualization
even more
soft reboot
cortex M separation kernel
secure boot
platform support
memory

user registers

time
Intro
School
Verification
More
Conclusion
Formal Verification of a Tiny Separation Kernel
take home
----------------

1. binary level

2. communication

3. bisimulation

4. incl. system

oliver@sics.se
oliver@sics.se
Full transcript