User loginNavigation |
archivesThe 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 identiï¬ed 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 | 12 comments | other blogs | 13215 reads
|
Browse archivesActive forum topics |
Recent comments
2 weeks 4 days ago
2 weeks 4 days ago
2 weeks 4 days ago
24 weeks 6 days ago
29 weeks 1 day ago
30 weeks 5 days ago
30 weeks 5 days ago
33 weeks 3 days ago
38 weeks 10 hours ago
38 weeks 11 hours ago