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_hackerdetecting_kernel_goes_open_source/ > >> 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) <[email protected]> > uid Cathal Garvey (Microstatus account) > <[email protected]> > uid Cathal Garvey (Gitorious code hosting account) > <[email protected]> > sub 4096R/65B3395F 2013-02-06 -- ---------------------------------------------------------------------------- Troy Benjegerdes 'da hozer' [email protected] 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
