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