I wonder what would happen if somebody offered $10000 to the first applied researcher to find a fault or security error. According to http://ertos.nicta.com.au/research/l4.verified/proof.pml, buffer overflows, memory leaks, and other issues are not present. Maybe people would give up if they don't gain some quick results, but it seems like you'd want to sanity-check the claims using alternate techniques.
- Steve _______________________________________________ Secure Coding mailing list (SC-L) SC-L@securecoding.org List information, subscriptions, etc - http://krvw.com/mailman/listinfo/sc-l List charter available at - http://www.securecoding.org/list/charter.php SC-L is hosted and moderated by KRvW Associates, LLC (http://www.KRvW.com) as a free, non-commercial service to the software security community. _______________________________________________
