Dailydave mailing list archives
Re: [ proof checking ] [ safer software ] [???]
From: nnp <version5 () gmail com>
Date: Thu, 27 Aug 2009 00:14:08 +0100
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<shane () security-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 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
_______________________________________________ Dailydave mailing list Dailydave () lists immunitysec com http://lists.immunitysec.com/mailman/listinfo/dailydave
Current thread:
- [ proof checking ] [ safer software ] [???] Arun Koshy (Aug 16)
- Re: [ proof checking ] [ safer software ] [???] Shane Macaulay (Aug 26)
- Re: [ proof checking ] [ safer software ] [???] nnp (Aug 26)
- Re: [ proof checking ] [ safer software ] [???] Shane Macaulay (Aug 26)