CertiKOS: A breakthrough toward hacker-resistant operating systems | Hacker News Reader

CertiKOS: A breakthrough toward hacker-resistant operating systems

news.yale.edu

119 pointsspankipants37 comments

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...

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.

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 [2] http://flint.cs.yale.edu/flint/publications/dscal-talk.pdf

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-yggdr..., and last year as SOSP FSCQ: http://sigops.org/sosp/sosp15/current/2015-Monterey/013-chen...

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. :)

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.

Can anyone more knowledgeable than me comment on whether I'm crazy to think 6500 lines seems amazingly tiny for a full blown hypervisor?!

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-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.

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

Note: Paper is in publications on bottom. You'll know it by title.

Formal verification (what this seems to be about) can be a nice tool to verify something adheres to a specification or that it has no e.g. buffer overflows.

But I think that is not really the big problem we have. I think it is operating system interfaces. By default a process is in its own address space and cannot do anything dangerous. It is only with the operating system API (which is the syscalls or an C API that uses syscalls) that it can do dangerous things like writing in the filesystem. Posix defines such an API which allows every program to do the same as the user running it. Windows does the same. This would be fine in a world where we can trust each program we run to not be malicious and to not be exploitable. Now we are trying to make those inherently unsafe APIs safe via sandboxing, but I guess that it is much easier to create a new API that is safe from the beginning.

This is orthogonal. But first, there are still buffer overflows, null pointer accesses & segmentation faults, etc. in the kernel happening. And this is a big problem!

But lets assume this is solved. Then a API can be checked for certain properties. You can specify what it means that something is read-only in an environment etc. And ensure that it is enforced by the operating system.

As example: the verification of seL4 not only guarantees avoidance of classical security holes (buffer overflows etc.) but also certain non-interference properties.

> But I think that is not really the big problem we have.

It is a really big problem and it needs to be solved. Did you miss this recent news?

http://www.theregister.co.uk/2016/10/21/linux_privilege_esca...

Formal verification isn't as limited as you suggest. The original use of formal verification for security in high-assurance security was analysis of security kernels for OS's showing that every state the system could be in was secure or fail-safe. Early attempts like UCLA Secure UNIX showed UNIX was impossible to secure because the API's inherently leaked and/or gave attackers opportunities. That's why high-assurance projects abandoned them in favor of security kernels with user-mode version of UNIX isolating those apps from others. Or did entirely new architectures. Mainstream IT and INFOSEC ignored these lessons with most of the failures you've seen resulting. They still argue even though one model worked consistently and one they build on didn't. ;)

Here's a summary of security kernel approach:

http://www.cse.psu.edu/~trj1/cse443-s12/docs/ch6.pdf

Unfortunately, the secure UNIX papers are paywalled. Here's another high-assurance project with sections illustrating issues with UNIX API and changes they had to make. That's back when it had dozens of sys calls.

http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.93....

After a while, the formal verification people got the tools working well enough to prove absence of certain types of problems in code itself rather than an abstract model of it. So, now you see them showing absence of buffer overflows, etc. There's also tools to do similar stuff for assembly and hardware languages. I saw one proof that went down to the gates. Capabilities gradually expanded from system-level properties to lowest-level properties.

What's the difference with this https://sel4.systems/?

I searched the conference paper for "sel4" and this result seems relevant to your question:

  A comparison of the performance of seL4 and mC2 is
  not straightforward since the verified mC2 kernel
  runs on a multicore x86 platform, while the verified
  seL4 kernel runs on ARMv6 and ARMv7 hardware and
  only supports single-core

Multicore is on the seL4 roadmap[0], albeit the proof is listed as TBD.

0: http://sel4.systems/Info/Roadmap/

The main difference is the verification/design method. seL4 does the abstract machine in Haskell, model in HOL, and final code in C. Both Haskell and C are shown equivalent. It took a ton of work. They also have to use these two tools for expressing all kinds of solutions they're not ideal for.

CertiKOS is using a DSL approach if it's same as paper I'm remembering. They design languages or proving techniques ideal to the type of thing they're working on: memory management, I/O, etc. They prove each individual component as easily as they can. Then they have some way of modeling the system as a whole and/or integrating those. Too early to judge but they seem more productive than L4 project was due to tooling benefits.

According to one of the talks I watched, they are moving towards using more domain-specific languages.

That's ambiguous. Are you talking about seL4 or CertiKOS people?

The seL4 team, they have taken this approach with their drivers and ext2 implementation. Apparently it is part of a more general strategy [0].

[0] https://archive.fosdem.org/2015/schedule/event/sel4/

Ok. Good they're doubling down on it.

> One of the main breakthroughs of CertiKOS is that it supports concurrency, meaning that it can simultaneously run multiple threads (small sequences of programmed instructions) on multiple central processing unit (CPU) cores.

Isn't this parallelism?

It is. The point here is that they have proven that this feature is hack-proof. This is extremely difficult. The article does not give much details, however, Andrew Appel is a very big name in the field.

> “Ten years ago, no one would predict that we could prove the correctness of a single-threaded kernel, much less a multi-core one."

So apparently it's a breakthrough in this context.

Yes, having access to multiple cores means that one can process some things faster. But performance is not the focus of this work, although that is a happy side effect. The focus is on correctness of concurrent code.

CertiKOS's model explicitly accounts for the presence of concurrent processors accessing memory in an arbitrarily interleaved fashion. In order to get the verification process to sign off on a particular architecture, all accesses to shared memory _must_ use the correct synchronization primitives and memory barriers, among other things.

Yes, I've seen them used as synonyms, even when, in my opinion, they are not.

For the record, what I (and others, and I assume the parent too) understand as concurrency is many threads in a single core (interleaved/evicted, scheduling, quanta, yadda yadda), while parallelism means running multiple tasks in multiple cores at once.

> For the record, what I (and others, and I assume the parent too) understand as concurrency is many threads in a single core (interleaved/evicted, scheduling, quanta, yadda yadda), while parallelism means running multiple tasks in multiple cores at once.

In computer science, concurrency is a system of non-deterministic interleaved components, parallelism is a deterministic performance enhancement for programs by running fragments of it simultaneously.

For the purposes of verification, non-deterministic interleaving is the truly challenging problem, so the paper's use of "concurrency" seems reasonable.

https://www.youtube.com/watch?v=cN_DpYBzKso

Rob Pike's talk on why 'Concurrency Is Not Parallelism'

Oops, that may not have been your question.

Ok, now we can run a verified OS on multiple cores. Now, what value has verified software which runs on buggy or (theoretically) compromised hardware?

In my opinion safe computing requires verified software AND verified hardware. Since proprietary SW/HW cannot be trusted in general truly safe computing vitally depend on open software and open hardware.

It is one (huge) step in the right direction. We are not there yet but solving part of the problem is improvement anyway.

HW exploits are harder then SW ones so the practical implication is more safety regardeless the closed HW/ quality SW is not perfect.

> Now, what value has verified software which runs on buggy or (theoretically) compromised hardware?

The vast majority of bugs and vulnerabilities are due to software, not hardware. There's tremendous value in pushing that boundary back to the hardware layer.

But does everyone know that there's tremendous value in pushing that boundary? Do they know that pushing the boundary has the best value? You should tell them how tremendous your value is. That you have the best value.

When hardware comes with multiple levels of firmware, there is hardly any difference.

A search for "linux" in NVD returned over 4,500 entries. "firmware" has barely 900. So I'd say there's definitely a meaningful difference, and operating system kernels have been used in firmware (Linux and L4 have at least), so formally verifying kernels can eliminate firmware vulnerabilities too.

Is this real software or some academic thing?

Just glancing at their site, I suspect it's real, however, I doubt it's interesting to us except as an academic example:

Only open source code I could find (and it's not linked from their site that I could find) is here, it's tooling: https://github.com/CertiKOS

For Coq, which is the proof system they use, but also for extending the CompCert verified C compiler, which requires a commercial licence if you use it beyond "evaluation, research and education purposes". And given the domain, and of course you have to talk to a salesman, I'm sure it's not cheap, 6 figures a seat in USD would not be out of the question if not likely, I'm sure it's 5 figures at minimum.

This is in part because this sort of software is inherently more expensive, and for the people who really need to use these sorts of tools, like those building airplanes, it's cheap at the price. But by basing it on CompCert, they've got what's likely to be a very high floor for playing the game they've not (yet) invited us to.

By comparison, seL4 is now totally free (well, GPLed, but that's not a problem for software like it), and part of that is because they actually tried CompCert, but there was an impedance mismatch in connecting it to their higher level stuff, so they went with Magnus Myreen and his approach of analyzing (GCC produced in this case) binary code and connecting that to the higher level proofs.

Does this mean no more jailbreaking for iOS and Android?

Reply on news.ycombinator.com