Re: [ proof checking ] [ safer software ] [???]

[Shane Macaulay <shane () security-objectives com>]

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
> Dailydave () lists immunitysec com
> http://lists.immunitysec.com/mailman/listinfo/dailydave
>
>   

_______________________________________________
Dailydave mailing list
Dailydave () lists immunitysec com
http://lists.immunitysec.com/mailman/listinfo/dailydave