4 ms·

I found the linked news piece as impenetrable as this project claims to be. Something just feels wrong about the organization of ideas. The conference paper (

I found the linked news piece as impenetrable as this project claims to be. Something just feels wrong about the organization of ideas. The conference paper (in pdf format) is located here: https://www.usenix.org/system/files/conference/osdi16/osdi16-gu.pdf https://www.usenix.org/system/files/conference/osdi16/osdi16... Section 2 of the paper seems to be a thorough and mostly readable overview of the project and was much more enlightening than the YaleNews piece. I didn't end up reading the remainder of the paper.

Animats 10y ago
That's a prettier version of the Yale paper.[1] Key points: - It's a hypervisor. It usually needs a guest OS on top, which is, inevitably, Linux. Code size of the hypervisor is about 6500 lines. The OS itself is written in some subset of C and in assembler. Both are formally verified against a specification, written in a formal specification language. - The big advance over L4 is that this kernel does concurrency. The verified version of L4 can't do that, and has one big kernel lock, because their proof system can't deal with concurrency. This is why L4 avoids passing long messages; it locks up the system. - I've been trying to find more about the specification language and the subset of C. There are some very simple examples here.[2] But in the examples, the spec is so close to the code that it's not interesting. I did some work on formal specification of an OS years ago (the KSOS referenced in the paper here), so I'm curious to see how they addressed this. - They haven't done a file system yet. (That's a good problem for formal specification, because the abstract semantics of a file system are simple; it's an efficient implementation that's hard.) [1] http://flint.cs.yale.edu/certikos/publications/certikos.pdf http://flint.cs.yale.edu/certikos/publications/certikos.pdf [2] http://flint.cs.yale.edu/flint/publications/dscal-talk.pdf http://flint.cs.yale.edu/flint/publications/dscal-talk.pdf
- jroesch 10y ago
  There have already been two file system verification projects, this year's OSDI best paper is the most recent example, http://locore.cs.washington.edu/papers/sigurbjarnarson-yggdrasil.pdf http://locore.cs.washington.edu/papers/sigurbjarnarson-yggdr..., and last year as SOSP FSCQ: http://sigops.org/sosp/sosp15/current/2015-Monterey/013-chen-online.pdf http://sigops.org/sosp/sosp15/current/2015-Monterey/013-chen...
  - nickpsecurity 10y ago
    Holy crap! That some great improvements together with the COGENT paper I posted in this sub-thread. I'd love to see them try to overlap in their strong suits. Push-button is hard to argue with, though. Thanks for the links. :)
- nano_o 10y ago
  Also, it seems they proved a behavioral equivalence property: any user-space program has exactly the same behaviors when running on the C+assembly implementation of the OS (6500 lines) and when running on the abstract machine specified by the high-level specification of the OS (450 lines). Their specification also includes liveness properties (e.g. no deadlocks or livelocks). For comparison, seL4 has verified behavioral refinement between implementation and specification, termination of all syscalls, and several security properties (non-interference and information-flow properties among threads), worst case execution times, and other things; but, seL4 does not support fined-grained concurrency.
- makmanalp 10y ago
  Can anyone more knowledgeable than me comment on whether I'm crazy to think 6500 lines seems amazingly tiny for a full blown hypervisor?!
  - nickpsecurity 10y ago
    Most software is bloated with lots of features and doing too much in privileged mode. High-assurance security field keeps our privileged software tiny pushing everything else into either user-mode or separate, privileged components with clean interfaces that are easy to verify. Before this, there were separation kernels like INTEGRITY-178B that was EAL6+ verified for security due to being similarly small & easy-to-analyze. seL4 took it to next level with code & ASM verification but lacks many EAL6+ requirements. This one intends to boost productivity of code-level verification with DSL's. http://www.ghs.com/products/safety_critical/integrity-do-178b.html http://www.ghs.com/products/safety_critical/integrity-do-178... Note: The initial reason for keeping it small was that the formal tools just couldn't handle anything beyond 10,000 loc. Now, it's believed they might handle up to 100,000 with enough composition. Already partial verification, esp code-level, of large programs like Hyper-V w/ VCC. Full formal is work in progress at that level with tools like these going to be quite useful.
- nickpsecurity 10y ago
  Far as filesystem part, you might be interested in COGENT. They did a basic verification of an ext2 filesystem coded in functional, system language with certified compilation: https://ts.data61.csiro.au/projects/TS/cogent.pml https://ts.data61.csiro.au/projects/TS/cogent.pml Note: Paper is in publications on bottom. You'll know it by title.

Animats 10y ago

That's a prettier version of the Yale paper.[1] Key points: - It's a hypervisor. It usually needs a guest OS on top, which is, inevitably, Linux. Code size of the hypervisor is about 6500 lines. The OS itself is written in some subset of C and in assembler. Both are formally verified against a specification, written in a formal specification language. - The big advance over L4 is that this kernel does concurrency. The verified version of L4 can't do that, and has one big kernel lock, because their proof system can't deal with concurrency. This is why L4 avoids passing long messages; it locks up the system. - I've been trying to find more about the specification language and the subset of C. There are some very simple examples here.[2] But in the examples, the spec is so close to the code that it's not interesting. I did some work on formal specification of an OS years ago (the KSOS referenced in the paper here), so I'm curious to see how they addressed this. - They haven't done a file system yet. (That's a good problem for formal specification, because the abstract semantics of a file system are simple; it's an efficient implementation that's hard.) [1] http://flint.cs.yale.edu/certikos/publications/certikos.pdf http://flint.cs.yale.edu/certikos/publications/certikos.pdf [2] http://flint.cs.yale.edu/flint/publications/dscal-talk.pdf http://flint.cs.yale.edu/flint/publications/dscal-talk.pdf

jroesch 10y ago
There have already been two file system verification projects, this year's OSDI best paper is the most recent example, http://locore.cs.washington.edu/papers/sigurbjarnarson-yggdrasil.pdf http://locore.cs.washington.edu/papers/sigurbjarnarson-yggdr..., and last year as SOSP FSCQ: http://sigops.org/sosp/sosp15/current/2015-Monterey/013-chen-online.pdf http://sigops.org/sosp/sosp15/current/2015-Monterey/013-chen...
- nickpsecurity 10y ago
  Holy crap! That some great improvements together with the COGENT paper I posted in this sub-thread. I'd love to see them try to overlap in their strong suits. Push-button is hard to argue with, though. Thanks for the links. :)
nano_o 10y ago
Also, it seems they proved a behavioral equivalence property: any user-space program has exactly the same behaviors when running on the C+assembly implementation of the OS (6500 lines) and when running on the abstract machine specified by the high-level specification of the OS (450 lines). Their specification also includes liveness properties (e.g. no deadlocks or livelocks). For comparison, seL4 has verified behavioral refinement between implementation and specification, termination of all syscalls, and several security properties (non-interference and information-flow properties among threads), worst case execution times, and other things; but, seL4 does not support fined-grained concurrency.
makmanalp 10y ago
Can anyone more knowledgeable than me comment on whether I'm crazy to think 6500 lines seems amazingly tiny for a full blown hypervisor?!
- nickpsecurity 10y ago
  Most software is bloated with lots of features and doing too much in privileged mode. High-assurance security field keeps our privileged software tiny pushing everything else into either user-mode or separate, privileged components with clean interfaces that are easy to verify. Before this, there were separation kernels like INTEGRITY-178B that was EAL6+ verified for security due to being similarly small & easy-to-analyze. seL4 took it to next level with code & ASM verification but lacks many EAL6+ requirements. This one intends to boost productivity of code-level verification with DSL's. http://www.ghs.com/products/safety_critical/integrity-do-178b.html http://www.ghs.com/products/safety_critical/integrity-do-178... Note: The initial reason for keeping it small was that the formal tools just couldn't handle anything beyond 10,000 loc. Now, it's believed they might handle up to 100,000 with enough composition. Already partial verification, esp code-level, of large programs like Hyper-V w/ VCC. Full formal is work in progress at that level with tools like these going to be quite useful.
nickpsecurity 10y ago
Far as filesystem part, you might be interested in COGENT. They did a basic verification of an ext2 filesystem coded in functional, system language with certified compilation: https://ts.data61.csiro.au/projects/TS/cogent.pml https://ts.data61.csiro.au/projects/TS/cogent.pml Note: Paper is in publications on bottom. You'll know it by title.