-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA384 Hi, first of all I want to discuss 'verification'. There are so many different definitions and it seems everybody uses their own definition. It is strongly connected to trusted code base. Which axioms of a rule system do you believe in? Do you believe that arithmetic is verified? There are some axioms which you need to trust... [http://mathworld.wolfram.com/GoedelsIncompletenessTheorem.html] Some software 'verification systems' trust in more axioms than others... and yes, there have been verification systems which accepted invalid code/proved falsity. The other topic is trusted code base: - verification system itself (it's just a piece of software) - compiler? [http://cm.bell-labs.com/who/ken/trust.html] - language runtime? - operating system? - microcode of the processor? - hardware?? On 01/19/2014 18:43, Hannes Frederic Sowa wrote:
MPX was already committed to gcc trunk, so I hope this situation could improve in future (it is reverted for 4.9 but I think it will come back after the release in March).
The difference, as far as I can tell is in-band vs out-of-band signalling... (correct me if I'm wrong) with the former you put some magic values before and after the array, and an attacker has to guess these. The latter puts the meta-information out of band, hard to predict for an attacker.. that's at least the difference between the llvm bounds checks plugin (BoundsChecking.cpp / MemorySanitizer.cpp in LLVM 3.3) and the softboundCETS approach..
I can recommend several languages: - coq (http://coq.inria.fr) [the tutorial software foundations http://www.cis.upenn.edu/~bcpierce/sf/ ] - agda (http://wiki.portal.chalmers.se/agda/pmwiki.php) - idris (http://www.idris-lang.org/)
Maybe you can comment a bit on the code extraction process into compilable languages.
[I've to admit that I did some research in Coq over the recent 3 years (a higher-order separation logic to verify the full functional correctness of Java programs). And no, at the moment I don't believe anymore in taking off-the-shelf code and verify its correctness. That's a myth. If we need to reimplement it anyways, why not in a neat modern programming language?] In Coq you can develop programs and extract them to ML code, without the irrelevant proof bits. But it seems this is rather cumbersome. The verified optimizing compiler for C, compcert [http://compcert.inria.fr/] does this. The softbound plugin [http://acg.cis.upenn.edu/softbound/], although they developed a semantics for the LLVM intermediate representation, have the real implementation in C++ and no formalized proof (at least I couldn't find any) of its correspondence to the Coq development. I actually think there are some overflows in the C++ runtime (size + start < bound might fail The verified L4 microkernel redeveloped a bunch of C++ and assembly into Haskell in order to be able to prove it. The main difference between Coq and Agda/Idris is that the dependent types are used in Coq to proof stuff, while in Agda/Idris you use them for programming. (Obviously, all is the same, and Adam wrote a great book about programming with dependent types in Coq http://adam.chlipala.net/cpdt/). Agda has a story about people not interested in executing programs, but rather type check and prove them. Idris has a slightly different tradeoff -- instead of forcing developers to write only total functions (due to curry-howard, partial functions better not be used for proofs [basically if you use a partial function for a proof, you assume false, and can prove everything]), but also partial functions. Only total ones can be used for proving though. Idris has a compiler which produces executable programs! :) Obviously the runtime needs to be looked into. In the end it is part of your trusted code base. Unfortunately I have not used ATS, but if I'm not entirely wrong, it is a dependently typed programming language with mutable state and a C foreign function interface which treats variables as resources (and uses linear logic/linear types to do so). A very interesting system; Chris Double wrote several blog posts when he used it http://bluishcoder.co.nz/tags/ats/ . I'm happy to discuss further, Hannes -----BEGIN PGP SIGNATURE----- Version: GnuPG v2.0.19 (FreeBSD) iQIcBAEBCQAGBQJS3Q4iAAoJELyJZYjffCjuuwAQAIlV480onmDrunNB5GOrRqXK EaEfbIQPRZT4tnaj9zrqjxAxgh+gls9ugKPKPaUfQzxzQUPSn88SWx6dpRKfGYZu e4N77kSCb1YoTnG9SjWao2IVRxnSZXtATmNAEQG8FqyXejbq+G1IJfP2eX9DRzM8 nLB1JQLWcI4lZonYYh2pIHA8n0raJav2OCqUhp7tbjEuubU2Uxil8ToHDMfaqzSY /hanRu/F9sCFVNtNOysIsbP8bUukZLex3yIgRIiojUy3S2872doqSL1QNeRa3A/Z aOifWowLi4UdCdcmk2obvdI4sSanh7LG5ijw9IZDXdOsWM4Jyb9qZS+PP0Rs6I6T IzHwA5wf+Te0q6Gh621W6bDnaR4dDd6cARmLafyGyY0ViRbWJoLjLW6d4zfXttvh V/dryq4LjdztlyblfjxY9Djlx2O8JO/Q7/YYhb8ZpOn8lek7cQH4FxZWGmWqpiEf Ay7A1nPM47BIPgKgTFRdMpeUnrttm+HMXOHtx9sID6jycT8HsJxOA645gunhi4D+ 5UhcKMNUZae2tiqxOeUsvxI9/YwZu7g2FLvgoR4h7koQfl1jpsbNxE2ckopc+2ej 1YQDF7ZB0gTXyX9xHRxSEb76fFBW1sPz0s/W5DTEnQw+DnT0LIXaNGsvzAE7RU/e GcMkqEodPLluzQJgPwz4 =xZP7 -----END PGP SIGNATURE-----