Home

The SAFE Platform

A. Dehon, B. Karel, B. Montagu, B. Pierce, J. Smith, T. Knight, S. Ray, G. Sullivan, G. Malecha, G. Morrisett, R. Pollack, R. Morisset & O. Shivers. Preliminary design of the SAFE platform. In Proceedings of the 6th Workshop on Programming Languages and Operating Systems (PLOS 2011). ACM, Oct. 2011.
ABSTRACT — Safe is a clean-slate design for a secure host architecture, coupling advances in programming languages, operating systems, and hardware, and incorporating formal methods at every step. The project is still at an early stage, but we have identified a set of fundamental architectural choices that we believe will work together to yield a high-assurance system. We sketch the current state of the design and discuss several of these choices.
Proving an operating system correct down to the hardware specification and against a threat model does seem to demand new programming languages and higher-order constructive type theory.
By Charles Stewart at 2011-09-12 11:41 | General | Type Theory | other blogs | 13443 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Tagged values

I find it surprising that they are tagging values with types and access controls at the hardware level. It seems to me that with a high level type system, most of those checks could be eliminated statically and thus it would be simpler (at least the hardware would be simpler) and more performant to do the checks in software only where you can't prove they aren't need.

By Matt M at Mon, 2011-09-12 14:15 | login or register to post comments

That puts more software in

That puts more software in the TCB.

By Ben L. Titzer at Tue, 2011-09-13 00:57 | login or register to post comments

But...

But isn't hardware more difficult and costly to verify than software? And they're planning to verify the hardware, so I still don't get it.

By Matt M at Tue, 2011-09-13 01:16 | login or register to post comments

Haven't read any of this...

Haven't read any of this... But isn't the typical issue that you need to be secure against machine code that bypasses the compilation tool chain?

By Ehud Lamm at Tue, 2011-09-13 02:18 | login or register to post comments

FPCC

Isn't that supposed to be addressed by Foundational Proof-Carrying Code and/or certified verifiers?

By Paul Snively at Tue, 2011-09-13 14:41 | login or register to post comments

These are solutions, yeah.

These are solutions, yeah. It means simple erasure is not possible, of course.

By Ehud Lamm at Tue, 2011-09-13 18:27 | login or register to post comments

No virtual memory

But isn't hardware more difficult and costly to verify than software?

My guess is the opposite. Note that the architecture does not have virtual memory, so they need a different model to ensure memory isolation.

By Charles Stewart at Tue, 2011-09-13 08:10 | login or register to post comments

(I'm one of the members of

(I'm one of the members of the SAFE team)
We're taking a "defense in depth" approach, where we apply static analysis to prove safety and correctness properties at all levels (app, compiler, OS), and we are _also_ performing fine-grained runtime access checks. It may seem like overkill. We're still unclear how fascist we'll be about using certified compilers for assembly/binary code actually executed. If we allow arbitrary ISA code, then of course we'll need the dynamic access checks.

By GregS at Thu, 2011-09-15 00:33 | login or register to post comments

biggest threats are from the same user

This is a really cool project. Based on a quick skim, they are using formal methods to build and verify a traditional Unix-like OS. Traditional Unix-like OSes are well understood these days, and there is very little innovation at levels below the user shell. At the same time, Unix is used as the foundations of quite a few software stacks. I'm glad someone is doing it.

If I may be forgiven one comment on the goal of the project, though, it's that the threat model traditional Unix OSes address is not the one that seems most problematic today. People today aren't losing data or leaking secrets because they share a multi-user machine and some other user on the machine attacks them. They lose data and secrecy due to downloading software and running it and that software taking advantage of them. The security problem I'd love to see more addressed is this agency problem. How do you run third-party software without totally losing your security?

The sad thing is that the state of the art is the web browser. Web browsers run right into this problem, and they've developed an ugly but effective system based around managed runtimes and the same-origin policy. Somehow I think we could do better than that, if only more of our best language and system designers were to take on the problem.

By lexspoon at Mon, 2011-09-19 14:35 | login or register to post comments

Ugly but INeffective

Most serious security papers about the state-of-the-art in mainstream Web browsers point out that there are still serious security flaws, largely due to shared address spaces (lack of memory encapsulation). I can't think of any papers off the top of my head, but they exist.

As far as state-of-the-art in research Web browsers go, I don't know if anyone has improved on the Combex DarpaBrowser built by Mark S. Miller as part of his Ph.D. thesis work.

Search tags (added, since your characterization of the problem above was not very search-friendly): ambient authorirty, confused deputy, multi-principal security, cross-site request forgery, object capability security, E programming language, Caja, secure third-party plug-in architecture, trustworthy computing from untrustworthy components.

Postscript: Morriset is also working on a verified DBMS, but his group has not yet tackled the most serious challenges for such a project. How hard would it be to find good abstractions that allow replacing much of the verified OS with a verified DBMS, such that there is no "file system"? Today, SAN architectures already mess around with the underlying storage done by the file system. e.g. Compellant's SAN offering recently acquired by Dell.

By Z-Bo at Mon, 2011-09-19 15:17 | login or register to post comments

not the standard Unix model

As I understand it, the high level language (as described in section 4.1) is meant to incorporate ideas from information-flow and capability-based systems, so they are not aiming for a traditional user-based discretionary security model. IF and capabilities should be helpful for isolating programs as well as users.

By Vilhelm Sjoberg at Tue, 2011-09-20 01:41 | login or register to post comments

I thought systems like

I thought systems like HiStar showed that, for the most part, legacy can remain? There was some discussion in the paper as well about reusing legacy..

By lmeyerov at Tue, 2011-09-20 05:23 | login or register to post comments