Alleged "microkernel mathematically proven to be bug free"

Troy Benjegerdes hozer at hozed.org
Tue Jul 29 07:31:11 PDT 2014


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




-- 
----------------------------------------------------------------------------
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




More information about the cypherpunks mailing list