Go read http://jvns.ca/blog/2014/03/12/the-rust-os-story/
and start writing your own malloc If we had a L4-compatible kernel written in Rust that would be pretty damn cool. Now I just need to find someone to bill to play with this... On Tue, Jul 29, 2014 at 03:58:25PM +0100, Cathal Garvey wrote: > Lol, I haven't even written "hello world" in it yet, but I believe this > is exactly the sort of future use-case Rust is for. Perhaps I'm > mistaken, but surely someone's dreamt up a more modern take on C with > memory safety that can be used instead? > > On 29/07/14 15:31, Troy Benjegerdes wrote: > > 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 > > > > > > > > > > -- > 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
