I'm setting up a system with SeL4. None of the systems you're suggesting have fo... | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

		microcolonel on Jan 24, 2015 \| parent \| context \| favorite \| on: Google discloses three severe vulnerabilities in A... I'm setting up a system with SeL4. None of the systems you're suggesting have formal proofs of correctness, and this one not only has such proofs, but is written in C.

geofft on Jan 25, 2015 [–]

What is the process for patching seL4? How does e.g. adding a parameter to an existing function affect the proof, and what's the process for proving additional predicates?

microcolonel on Jan 26, 2015 | [–]

The proofs are publicly available, though I can imagine there would be significant... overhead involved in adding functions to the system.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact