6 ms·

Automated Verification of a Type-Safe Operating System [pdf]

122 points by muraiki 9y ago

sanxiyn 9y ago
Keyword here is "automated". Quoting, "In the end, the Verve design, implementation, and verification described in this paper took just 9 person-months, spread between two people". This is considerably less than, say, seL4, which took 20 person-years(!). Well, seL4 is larger than Verve, but still.
cjdrake 9y ago
Reminded me of this bit from Guido van Rossum's PyCon 2012 keynote: https://youtu.be/EBRMq2Ioxsc?t=1374 https://youtu.be/EBRMq2Ioxsc?t=1374 "I know my operating system kernel will never be proven correct."
- kmicklas 9y ago
  Of course he believes that, he's the creator of a language that doesn't even have a type system...
  - olewhalehunter 9y ago
    well it kind of does but idiomatic python is not very functional
    - eru 9y ago
      What does that have to do with functional programming? (I know Python3 has some optional gradual typing. And I know that Python ain't very functional---especially if you go by how Guido wants Python to be written. But I still don't see the connection---apart from that functional programming and academic theory on typing go hand-in-hand.)
  - Retra 9y ago
    It does, he just didn't want to attach it very strongly to his naming system
- fulafel 9y ago
  He is very probably right.
- nickpsecurity 9y ago
  There's two assertions: 1. They're not proving anything relevant to current software development. That's a joke to anyone following formal verification. Key protocols, microkernels, hypervisors, safe concurrency, CompCert compiler, part of NaCl, Microsoft's static verification for device drivers... the list gets bigger every year. Quite a few are already practical. 2. I know my operating system will never be proven correct. That's probably true if he uses one not designed for verification. The high-assurance field gave up on UNIX after prototypes like UCLA Secure UNIX and even Mach work showed it was inherently too complex and leak-prone to secure in a high-assurance way. They moved to security kernels, separation kernels, language runtimes, trustworthy hardware, and so on. Each time, tried to make the trusted part as correct and secure as possible. If they couldn't, a recovery option was added. So, we have numerous secure and high-uptime systems deployed whose methods were published even if source wasn't. He or others can always build on these if they want to replicate the results. His OS will at least be secure against most attacks, quite reliable in practice, and most errors recoverable with the rest not leading to data loss if good backup/restore plan. Good enough for me. :)
  - Blaisorblade0 9y ago
    > So, we have numerous secure and high-uptime systems deployed whose methods were published even if source wasn't. He or others can always build on these if they want to replicate the results. I know that's technically true, but not helpful, and that's why this line of thinking is becoming unfashionable. As a researcher in Programming Languages, who publishes and has reviewed code: By that argument, there's no need to publish CompCert or Coq, which seems ridiculous. Publishing code can help adoption even if the code gets rewritten. Publications without code often fail replication for many reasons (not necessarily involving foul play or even errors). I can't document all tricks needed to get the performance results in 20 pages. And replication in another scenario might show the results don't generalize easily (and nobody knew). So having sources provides the extra confidence you need before bothering. And compared to other publications without code, the needed expertise seems much less common. OTOH, papers do get used by the research community, possibly steering it in some direction (including then wrong one). And a few papers matter enough that people will attempt replication anyway (and learn if they work). When the results of a paper are "here's what we tried and got, new ideas are needed" (honestly, many papers on hard problems) then maybe sources don't matter.
Animats 9y ago
(2010) Whatever happened to that? Several papers in 2010, then nothing. Wikipedia says there was a 2013 release. Microsoft had a later project, Ironclad (2014) which built on that to build some simple applications.[1] That's an active project at Microsoft.[2] [1] https://www.usenix.org/system/files/conference/osdi14/osdi14-paper-hawblitzel.pdf https://www.usenix.org/system/files/conference/osdi14/osdi14... [2] https://www.microsoft.com/en-us/research/project/ironclad/# https://www.microsoft.com/en-us/research/project/ironclad/#
- gsnedders 9y ago
  Quite possibly the same that has happened to other OSes at MSR like Singularity and Midori: the team moved on to a new research project which involved writing another new OS.
  - pjmlp 9y ago
    I keep hoping one day such projects will have right level of management support and actually deliver something big into the mainstream. We got .NET Native, async/await, W10 pico-processes, secure kernel,windows internal refactoring... out of those projects, but they still feel they could have been much more with the right amount of management support.
- Someone 9y ago
  "Whatever happened to that?" Isn't the simple answer "Microsoft had a later project, Ironclad (2014) which built on that to build some simple applications."? Chris Hawblitzel worked on both projects. However, I wonder about your claim "That's an active project at Microsoft". Last publication on that page is from 2015, and last fit commit is from a year ago.
- nickpsecurity 9y ago
  As "Someone" said, they moved onto another project: https://www.usenix.org/system/files/conference/osdi14/osdi14-paper-hawblitzel.pdf https://www.usenix.org/system/files/conference/osdi14/osdi14...
Animats 9y ago
It's disappointing that little verified OSs like these don't show up little boxes that need them, such as home DSL routers, printers, webcams, and various IoT devices. Those all have one job, and run a fixed program or programs. You want them to do that one job and nothing else. Not act as attack vectors against other systems.
- eru 9y ago
  I think seL4 saw some adoption in routers?
  - nickpsecurity 9y ago
    I'd like a source on that since I try to collect examples of high-assurance security developed or adopted. Especially adopted as it's so rare.
    - im_down_w_otp 9y ago
      seL4 so far makes a lot of sense for what we're working on. The hardest part is finding seL4 expertise.
      - nickpsecurity 9y ago
        What you need is embedded microkernel expertise with some training in INFOSEC. Look up Nizza Secure-Systems Architecture paper for how to use such architectures well.
      - harry8 9y ago
        https://cog.systems/about/ https://cog.systems/about/
    - eru 9y ago
      MirageOS is another project to look into. I don't think it's high-assurance by itself, but it attracts the kind of people who are into that sort of thing. (HalVM, too.)

122 points by muraiki 9y ago

Keyword here is "automated". Quoting, "In the end, the Verve design, implementation, and verification described in this paper took just 9 person-months, spread between two people". This is considerably less than, say, seL4, which took 20 person-years(!). Well, seL4 is larger than Verve, but still.

cjdrake 9y ago

Reminded me of this bit from Guido van Rossum's PyCon 2012 keynote: https://youtu.be/EBRMq2Ioxsc?t=1374 https://youtu.be/EBRMq2Ioxsc?t=1374 "I know my operating system kernel will never be proven correct."

kmicklas 9y ago
Of course he believes that, he's the creator of a language that doesn't even have a type system...
- olewhalehunter 9y ago
  well it kind of does but idiomatic python is not very functional
  - eru 9y ago
    What does that have to do with functional programming? (I know Python3 has some optional gradual typing. And I know that Python ain't very functional---especially if you go by how Guido wants Python to be written. But I still don't see the connection---apart from that functional programming and academic theory on typing go hand-in-hand.)
- Retra 9y ago
  It does, he just didn't want to attach it very strongly to his naming system
fulafel 9y ago
He is very probably right.
nickpsecurity 9y ago
There's two assertions: 1. They're not proving anything relevant to current software development. That's a joke to anyone following formal verification. Key protocols, microkernels, hypervisors, safe concurrency, CompCert compiler, part of NaCl, Microsoft's static verification for device drivers... the list gets bigger every year. Quite a few are already practical. 2. I know my operating system will never be proven correct. That's probably true if he uses one not designed for verification. The high-assurance field gave up on UNIX after prototypes like UCLA Secure UNIX and even Mach work showed it was inherently too complex and leak-prone to secure in a high-assurance way. They moved to security kernels, separation kernels, language runtimes, trustworthy hardware, and so on. Each time, tried to make the trusted part as correct and secure as possible. If they couldn't, a recovery option was added. So, we have numerous secure and high-uptime systems deployed whose methods were published even if source wasn't. He or others can always build on these if they want to replicate the results. His OS will at least be secure against most attacks, quite reliable in practice, and most errors recoverable with the rest not leading to data loss if good backup/restore plan. Good enough for me. :)
- Blaisorblade0 9y ago
  > So, we have numerous secure and high-uptime systems deployed whose methods were published even if source wasn't. He or others can always build on these if they want to replicate the results. I know that's technically true, but not helpful, and that's why this line of thinking is becoming unfashionable. As a researcher in Programming Languages, who publishes and has reviewed code: By that argument, there's no need to publish CompCert or Coq, which seems ridiculous. Publishing code can help adoption even if the code gets rewritten. Publications without code often fail replication for many reasons (not necessarily involving foul play or even errors). I can't document all tricks needed to get the performance results in 20 pages. And replication in another scenario might show the results don't generalize easily (and nobody knew). So having sources provides the extra confidence you need before bothering. And compared to other publications without code, the needed expertise seems much less common. OTOH, papers do get used by the research community, possibly steering it in some direction (including then wrong one). And a few papers matter enough that people will attempt replication anyway (and learn if they work). When the results of a paper are "here's what we tried and got, new ideas are needed" (honestly, many papers on hard problems) then maybe sources don't matter.

Animats 9y ago

(2010) Whatever happened to that? Several papers in 2010, then nothing. Wikipedia says there was a 2013 release. Microsoft had a later project, Ironclad (2014) which built on that to build some simple applications.[1] That's an active project at Microsoft.[2] [1] https://www.usenix.org/system/files/conference/osdi14/osdi14-paper-hawblitzel.pdf https://www.usenix.org/system/files/conference/osdi14/osdi14... [2] https://www.microsoft.com/en-us/research/project/ironclad/# https://www.microsoft.com/en-us/research/project/ironclad/#

gsnedders 9y ago
Quite possibly the same that has happened to other OSes at MSR like Singularity and Midori: the team moved on to a new research project which involved writing another new OS.
- pjmlp 9y ago
  I keep hoping one day such projects will have right level of management support and actually deliver something big into the mainstream. We got .NET Native, async/await, W10 pico-processes, secure kernel,windows internal refactoring... out of those projects, but they still feel they could have been much more with the right amount of management support.
Someone 9y ago
"Whatever happened to that?" Isn't the simple answer "Microsoft had a later project, Ironclad (2014) which built on that to build some simple applications."? Chris Hawblitzel worked on both projects. However, I wonder about your claim "That's an active project at Microsoft". Last publication on that page is from 2015, and last fit commit is from a year ago.
nickpsecurity 9y ago
As "Someone" said, they moved onto another project: https://www.usenix.org/system/files/conference/osdi14/osdi14-paper-hawblitzel.pdf https://www.usenix.org/system/files/conference/osdi14/osdi14...

Animats 9y ago

It's disappointing that little verified OSs like these don't show up little boxes that need them, such as home DSL routers, printers, webcams, and various IoT devices. Those all have one job, and run a fixed program or programs. You want them to do that one job and nothing else. Not act as attack vectors against other systems.

eru 9y ago
I think seL4 saw some adoption in routers?
- nickpsecurity 9y ago
  I'd like a source on that since I try to collect examples of high-assurance security developed or adopted. Especially adopted as it's so rare.
  - im_down_w_otp 9y ago
    seL4 so far makes a lot of sense for what we're working on. The hardest part is finding seL4 expertise.
    - nickpsecurity 9y ago
      What you need is embedded microkernel expertise with some training in INFOSEC. Look up Nizza Secure-Systems Architecture paper for how to use such architectures well.
    - harry8 9y ago
      https://cog.systems/about/ https://cog.systems/about/
  - eru 9y ago
    MirageOS is another project to look into. I don't think it's high-assurance by itself, but it attracts the kind of people who are into that sort of thing. (HalVM, too.)