When you can write an interrupt or page fault handler in rust, let me know. On Tue, Jul 29, 2014 at 02:03:28PM +0100, Cathal Garvey wrote:
That seems suspect. Most obvious security flaws in C are due to misimplemented C, right? Not the algorithms themselves? So the kernel can be theoretically secure but still be packed with buffer overflows and pointer errors?
I'll wait until someone redoes it in a language designed for safe systems programming, like Rust. :)
On 29/07/14 13:41, Georgi Guninski wrote:
I didn't spend much time on this, just browsed some proofs. The proofs appear to not depend to on the C code AFAICT. Would trojanizing the C code invalidate the proofs?
The haskell stuff appear to not contain all info about the C code.
On Mon, Jul 28, 2014 at 06:26:50PM +0300, Georgi Guninski wrote:
news: http://www.theregister.co.uk/2014/07/28/aussie_droneprotecting_hackerdetecti... site: http://sel4.systems/
AFAICT they used Isabelle for the proofs.
Coq sucks much (not counting its developers).
-- T: @onetruecathal, @IndieBBDNA P: +353876363185 W: http://indiebiotech.com
pub 4096R/988B9099 2013-02-06 Cathal Garvey (Other accs: onetruecathal@twitter, cathalgarvey@github, cathalgarvey@gitorious, indiebiotech.com) <cathalgarvey@cathalgarvey.me> uid Cathal Garvey (Microstatus account) <onetruecathal@twitter.com> uid Cathal Garvey (Gitorious code hosting account) <cathalgarvey@gitorious.org> sub 4096R/65B3395F 2013-02-06
-- ---------------------------------------------------------------------------- Troy Benjegerdes 'da hozer' hozer@hozed.org 7 elements earth::water::air::fire::mind::spirit::soul grid.coop Never pick a fight with someone who buys ink by the barrel, nor try buy a hacker who makes money by the megahash