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

https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/pldi117-yang.pdf

by muraiki • 9 years ago

122 31 9 years ago

sanxiyn• 9 years 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• 9 years ago

Reminded me of this bit from Guido van Rossum's PyCon 2012 keynote:

https://youtu.be/EBRMq2Ioxsc?t=1374

"I know my operating system kernel will never be proven correct."

kmicklas• 9 years ago

Of course he believes that, he's the creator of a language that doesn't even have a type system...

olewhalehunter• 9 years ago

well it kind of does but idiomatic python is not very functional

Retra• 9 years ago

It does, he just didn't want to attach it very strongly to his naming system

fulafel• 9 years ago

He is very probably right.

nickpsecurity6• 9 years 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. :)

Blaisorblade02• 9 years 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.

Animats2• 9 years 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... [2] https://www.microsoft.com/en-us/research/project/ironclad/#

gsnedders• 9 years 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.

pjmlp4• 9 years 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• 9 years 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.

nickpsecurity6• 9 years ago

As "Someone" said, they moved onto another project:

https://www.usenix.org/system/files/conference/osdi14/osdi14...

Animats2• 9 years 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.

eru4• 9 years ago

I think seL4 saw some adoption in routers?

nickpsecurity6• 9 years 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.

ktta3• 9 years ago

The interesting this out of all this is that Microsoft is the one often doing research like this, from F*, Project Everest, to complete kernels, but I've yet to see Windows have any of the new techniques/tools arising from MSR.

I wonder if it is a problem of the research being fairly new, or a lack of software developers inside Microsoft willing to replace their existing code and learn new tools and languages.

pjmlp4• 9 years ago

Because you are not looking into the right spots:

- Windows 7 kernel reorganization

- MDIL .NET AOT compiler for Windows 8 and .NET Native for UWP

- async/await for .NET

- generics for .NET

- UWP based on COM (original idea was called ExtVOS before .NET existed)

- Task Programming Library for .NET

- Pico-processes on Windows 10

- Secure kernel on Windows 10

- Hyper-V based containers

- Driver verification framework using a theorem proving framework

- The P language used for writing Windows 8 USB drivers

I guess they just don't adopt more due to management, and how the windev and devtools relate to each other in regards to technology adoption.

Blaisorblade02• 9 years ago

Until recently, MSR was also very disconnected from product development. There was a distinct change last year.

Also, in general most papers are more useful for writing further papers to improve on their limitations (until something's great), than to be adopted right away. This one is pretty cool, but both the conclusion and the benchmarks set out significant challenges for further research. After all, this is the first OS using automated verification, not the last.

a lack of software developers inside Microsoft willing to replace their existing code and learn new tools and languages.

I'm sure research on the topic hasn't ended, so should they switch now or wait for more research? Or wait for research on verifying existing code? And if a new paper comes out, should they switch again? Also, do universities train enough developers to use such technology?

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

Related Stories