Alleged "microkernel mathematically proven to be bug free"

Cathal Garvey cathalgarvey at cathalgarvey.me
Tue Jul 29 07:58:25 PDT 2014


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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: 0x988B9099.asc
Type: application/pgp-keys
Size: 6176 bytes
Desc: not available
URL: <http://lists.cpunks.org/pipermail/cypherpunks/attachments/20140729/f8c88359/attachment-0001.key>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 901 bytes
Desc: OpenPGP digital signature
URL: <http://lists.cpunks.org/pipermail/cypherpunks/attachments/20140729/f8c88359/attachment-0001.sig>


More information about the cypherpunks mailing list