Memory and Type Safety in System Design

Safe to the Last Instruction:
Automated Verification of a
Type-Safe Operating System
Jean Yang
MIT CSAIL
Chris
 Hawblitzel
Microsoft Research
Safe to the Last Instruction:
Automated Verification of a
Type-Safe Operating System
Jean Yang
MIT CSAIL
Chris
 Hawblitzel
Microsoft Research
3
Safe to the Last Instruction / Jean Yang
Safe to the Last Instruction / Jean Yang
4
Safe to the Last Instruction / Jean Yang
Memory Safety
5
Type Safety
6
Safe to the Last Instruction / Jean Yang
Safe to the Last Instruction / Jean Yang
Untyped
Unsafe code
(GC, stacks, drivers, …)
Type-checked OS
File
System
Drivers
Applications
Microkernel
Hardware
Previously: “Safe” Systems
7
 
What
currently
exists
Safe to the Last Instruction / Jean Yang
Untyped
Unsafe code
(GC, stacks, drivers, …)
Type-checked OS
File
System
Drivers
Applications
Microkernel
Hardware
End-to-End Safe Systems
8
Verified code
(GC, stacks, drivers, …)
 
What we
want
Verified
Type-checked
Verve, a Type-Safe OS
Safe to the Last Instruction / Jean Yang
 
Verify 
partial
correctness 
of low-
level 
Nucleus
 
using
Hoare logic based on a
hardware spec
.
Verify an
 interface to
typed assembly 
for
end-to-end safety
.
Nucleus
File
System
Drivers
Applications
Microkernel
Hardware specification
Interface specification
9
The Verve Nucleus
Safe to the Last Instruction / Jean Yang
10
 
    x86 instructions
Memory bounds
 
Devices
GC Heap
 
Allocator and GC
[POPL 2009]
 
Stacks
Interrupt
table
 
Interrupt/error handling
Interface specification
Thread Context Invariant
 
function
 
StateInv
  
(s
:StackID
, state
:StackState
, …)
   
returns
(bool) {
   (
!IsEmpty
(state) 
&& (
IsInterrupted
(state) 
&& (
IsYielded
(state) 
 
&& state == 
StackYielded
(
  
  
StackEbp
(s, tMems)
  
, 
StackEsp
(s, tMems) + 4
  
, 
StackRA
(s, tMems, fMems)) && …
}
Safe to the Last Instruction / Jean Yang
11
“Load” Specification
 
procedure
 
Load(ptr
:
int
)
 
returns
 
(val
:
int
);
 
requires
 
memAddr
(ptr);
 
requires
 
Aligned
(ptr);
 
modifies
 
Eip;
 
ensures
 
word
(val);
 
ensures
 
val == Mem[ptr];
Safe to the Last Instruction / Jean Yang
12
Assembling Verve
Verified
Safe to the Last Instruction / Jean Yang
Boogie/Z3
Translator/
Assembler
Source file
 
Compilation tool
Verification tool
Nucleus.bpl (x86)
13
Boogie to x86
 
implementation
 ReadKeyboard(){
 
call
 KeyboardStatusIn8();
 
call
 eax := And(eax, 1);
 
if (eax != 0) { 
goto
 proc; }
 
call
 eax := mov(256);
 
return;
 
proc:
 
call
 KeyboardDataIn8();
 
call
 eax := And(eax, 255);
 
return;
}
Safe to the Last Instruction / Jean Yang
 
ReadKeyboard proc
 
in
 al, 064h
 
and
 eax, 1
 
cmp eax, 0
 
jne 
ReadKeyboard$proc
 
mov eax, 256
 
ret
ReadKeyboard
$skip:
 
in al, 060h
 
and eax, 255
 
ret
14
Building Verve
Verified
Safe to the Last Instruction / Jean Yang
C# compiler
Kernel.cs
Boogie/Z3
Translator/
Assembler
TAL checker
Linker/ISO generator
Verve.iso
Source file
Compilation tool
Verification tool
Nucleus.bpl (x86)
Kernel.obj (x86)
15
Verve Performance
Safe to the Last Instruction / Jean Yang
16
Low Annotation Burden
Safe to the Last Instruction / Jean Yang
17
 
9 person-months
 
3x code
Verve vs. SeL4?
Safe to the Last Instruction / Jean Yang
SeL4
Verified microkernel
8,700 lines of C
 
200,000
 lines of Isabelle
~600 lines ARM assembly
 
120-240 person-months
18
 
20x code
Verve
Verified Nucleus
~1500 lines of x86
C# kernel
Contributions
Safe to the Last Instruction / Jean Yang
First 
automatically,
mechanically verified
OS
 
for
 
type safety
.
Real system 
running on
x86 with 
efficient code
.
Approach  for using
automated techniques
to verify safety.
Verified
Type-checked
Verified nucleus
File
System
Drivers
Applications
Microkernel
Hardware specification
Interface specification
 
http://www.codeplex.com/
singularity
19
Slide Note
Embed
Share

Explore the concept of ensuring memory and type safety in system design, featuring safe systems, verified code, hardware specifications, and end-to-end safety measures. Learn about Verve, a type-safe OS, and the Verve Nucleus designed for partial correctness and safety verification at the hardware level.


Uploaded on Oct 11, 2024 | 0 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


  1. Safe to the Last Instruction: Jean Yang MIT CSAIL Chris Hawblitzel Microsoft Research

  2. Safe to the Last Instruction: Jean Yang MIT CSAIL Chris Hawblitzel Microsoft Research

  3. Safe to the Last Instruction / Jean Yang 3

  4. Safe to the Last Instruction / Jean Yang 4

  5. Memory Safety Safe to the Last Instruction / Jean Yang 5

  6. Type Safety Safe to the Last Instruction / Jean Yang 6

  7. Previously: Safe Systems Type-checked OS Applications File System Drivers Microkernel What currently exists Untyped Unsafe code (GC, stacks, drivers, ) Hardware Safe to the Last Instruction / Jean Yang 7

  8. End-to-End Safe Systems Type-checked OS Applications File System Drivers Microkernel What we want Untyped Unsafe code (GC, stacks, drivers, ) (GC, stacks, drivers, ) Verified code Hardware Safe to the Last Instruction / Jean Yang 8

  9. Verve, a Type-Safe OS Verify partial correctness of low- level Nucleus using Hoare logic based on a hardware spec. Verify an interface to typed assembly for end-to-end safety. Applications Type-checked File System Drivers Microkernel Interface specification Verified Nucleus Hardware specification Safe to the Last Instruction / Jean Yang 9

  10. The Verve Nucleus Applications Interface specification Interface specification Type-checked Verified File System Drivers Interrupt table Microkernel GC Heap Interrupt/error handling Interface specification Allocator and GC [POPL 2009] Stacks Verified x86 instructions Memory bounds Nucleus Devices Hardware specification Safe to the Last Instruction / Jean Yang 10

  11. Thread Context Invariant function StateInv (s:StackID, state:StackState, ) returns(bool) { (!IsEmpty(state) && (IsInterrupted(state) && (IsYielded(state) && state == StackYielded( StackEbp(s, tMems) , StackEsp(s, tMems) + 4 , StackRA(s, tMems, fMems)) && } Safe to the Last Instruction / Jean Yang 11

  12. Load Specification procedureLoad(ptr:int) returns(val:int); requiresmemAddr(ptr); requiresAligned(ptr); modifies Eip; ensuresword(val); ensuresval == Mem[ptr]; Safe to the Last Instruction / Jean Yang 12

  13. Assembling Verve Source file Verification tool Compilation tool Verified Nucleus.bpl (x86) Boogie/Z3 Translator/ Assembler Safe to the Last Instruction / Jean Yang 13

  14. Boogie to x86 implementation ReadKeyboard(){ call KeyboardStatusIn8(); call eax := And(eax, 1); if (eax != 0) { goto proc; } call eax := mov(256); return; proc: call KeyboardDataIn8(); call eax := And(eax, 255); return; } ReadKeyboard proc in al, 064h and eax, 1 cmp eax, 0 jne ReadKeyboard$proc mov eax, 256 ret ReadKeyboard$skip: in al, 060h and eax, 255 ret Safe to the Last Instruction / Jean Yang 14

  15. Building Verve Source file Verification tool Kernel.cs Compilation tool C# compiler Verified Nucleus.bpl (x86) Kernel.obj (x86) Boogie/Z3 TAL checker Translator/ Assembler Linker/ISO generator Verve.iso Safe to the Last Instruction / Jean Yang 15

  16. Verve Performance Verve Cycles Comparisons Cycles functionality Round-trip L4 (IPC) 224 98 yield SeL4 (IPC) 448 Round-trip wait + signal 216 Singularity (yield) 2156 Linux (yield) 2390 Windows (yield) 3554 Safe to the Last Instruction / Jean Yang 16

  17. Low Annotation Burden Copying Mark-sweep 1185 4309 Specification Boogie lines Verified Boogie lines 4854 3x code x86 instructions 1377 1489 9 person-months Safe to the Last Instruction / Jean Yang 17

  18. Verve vs. SeL4? Applications File System Drivers 120-240 person-months SeL4 Verified microkernel C# kernel Verve 8,700 lines of C Verified Nucleus ~1500 lines of x86 ~600 lines ARM assembly 200,000 lines of Isabelle 20x code Safe to the Last Instruction / Jean Yang 18

  19. Contributions First automatically, mechanically verified OSfor type safety. Real system running on x86 with efficient code. Approach for using automated techniques to verify safety. Applications Type-checked File System Drivers Microkernel Interface specification Verified Verified nucleus Hardware specification http://www.codeplex.com/singularity Safe to the Last Instruction / Jean Yang 19

More Related Content

giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#giItT1WQy@!-/#