Alleged "microkernel mathematically proven to be bug free"

[Troy Benjegerdes]

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 at twitter, cathalgarvey at github, cathalgarvey at gitorious, indiebiotech.com) <cathalgarvey at cathalgarvey.me>
> >> uid                            Cathal Garvey (Microstatus account) <onetruecathal at twitter.com>
> >> uid                            Cathal Garvey (Gitorious code hosting account) <cathalgarvey at gitorious.org>
> >> 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 at twitter, cathalgarvey at github, cathalgarvey at gitorious, indiebiotech.com) <cathalgarvey at cathalgarvey.me>
> uid                            Cathal Garvey (Microstatus account) <onetruecathal at twitter.com>
> uid                            Cathal Garvey (Gitorious code hosting account) <cathalgarvey at gitorious.org>
> sub  4096R/65B3395F 2013-02-06




-- 
----------------------------------------------------------------------------
Troy Benjegerdes                 'da hozer'                  hozer at 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