From: nnp (version5gmail.com)
Date: Wed Aug 26 2009 - 18:14:08 CDT

• Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

As far as I can tell there was no verification done by a compiler. The
paper [1] describes the technique (sort of). It's a refinement proof
from an abstract specification to C code.

[1] http://ertos.nicta.com.au/publications/papers/Klein_EHACDEEKNSTW_09.pdf

On Wed, Aug 26, 2009 at 1:40 PM, Shane
Macaulay<shanesecurity-objectives.com> wrote:
> Looks interesting, reminiscent of http://singularity.codeplex.com/, also
> on codeplex is a series of tools, http://ccimetadata.codeplex.com/ and
> http://vcc.codeplex.com/, also http://llvm.org is fairly mature, some
> other related projects can also be found via those links.  Full source
> included.  I'm stressing that point as I was not able to find the
> compiler the team used to validate their 7500 lines of C code.  If it
> is, I'd be interested to toy with it and have yet to find a system,
> aforementioned tools included, which lived up to the hype.  Often
> evading the question by only supporting subset's of C (for the truly
> motivated http://www.aitcnet.org/isai/) or whatever other restricted
> scope ;), I believe I've used these tools all correctly and have
> produced working test cases which appear to validate or check the
> various tutorials or guides included, yet I've found it possible to
> construe valid C code which happily compiles and runs and evades
> AST/model checker logic, resulting in silent failures.  I suppose the
> 7500 lines of C code was actually, 7500 lines of C* (astrix'd -- our C
> dialect and we made sure to not get too tricky with our syntax),
> nevertheless looks cool, but like I said, would be neat to see the compiler.
>
> Real technical security, highly nuanced, does not lend itself well for
> abstraction's.  Perceived technical security, well, that's another
> matter entirely.
>
>
> Arun Koshy wrote:
>> check :
>>
>> http://ertos.nicta.com.au/research/l4.verified/
>>
>> media etc :
>>
>> http://www.theengineer.co.uk/Articles/312631/Safer+software.htm
>>
>> Of course, the work is based on a set of interesting assumptions and
>> fairly delimited universe ( given the understandable need to restrict
>> scope ). Comments anyone ?
>> _______________________________________________
>> Dailydave mailing list
>> Dailydavelists.immunitysec.com
>> http://lists.immunitysec.com/mailman/listinfo/dailydave
>>
>>
>
> _______________________________________________
> Dailydave mailing list
> Dailydavelists.immunitysec.com
> http://lists.immunitysec.com/mailman/listinfo/dailydave
>
_______________________________________________
Dailydave mailing list
Dailydavelists.immunitysec.com
http://lists.immunitysec.com/mailman/listinfo/dailydave

• Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]