HN Gopher Feed (2017-07-10) - page 1 of 10
 
___________________________________________________________________
Automated Verification of a Type-Safe Operating System [pdf]
91 points by muraiki
https://www.microsoft.com/en-us/research/wp-content/uploads/2016...
___________________________________________________________________
 
sanxiyn - 6 hours 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.
 
Animats - 1 hours 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 - 1 hours ago
  I think seL4 saw some adoption in routers?
 
cjdrake - 5 hours 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 - 4 hours ago
  Of course he believes that, he's the creator of a language that
  doesn't even have a type system...
 
    olewhalehunter - 3 hours ago
    well it kind of does but idiomatic python is not very
    functional
 
      eru - 1 hours 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.)
 
  fulafel - 4 hours ago
  He is very probably right.
 
Animats - 5 hours 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 - 5 hours 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 - 4 hours 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 - 5 hours 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.