3 ms·

Thanks for the info, did some searching based on your comment and I managed to find a report made by Altran/Praxis detailing the development process and technol

Thanks for the info, did some searching based on your comment and I managed to find a report made by Altran/Praxis detailing the development process and technologies for a tokeneer ID station implementation they did for the NSA. Very interesting stuff. http://www.adacore.com/uploads/downloads/Tokeneer_Report.pdf http://www.adacore.com/uploads/downloads/Tokeneer_Report.pdf It really shows the amount of resources and knowledge required for actually having safe or secure systems.

nickpsecurity 10y ago
Glad you enjoyed it. Remember Praxis' method next time some fool says you can't engineer software. A few companies like them do. They're now just called Altran. The Tokeneer link was good since they published the source code on AdaCore website for people to learn from. However, the highest-security thing they did was the CA below under UK equivalent of EAL6/7. http://www.anthonyhall.org/c_by_c_secure_system.pdf http://www.anthonyhall.org/c_by_c_secure_system.pdf Example of new one for model-to-code-to-ASM verification https://www.umsec.umn.edu/sites/www.umsec.umn.edu/files/hardin-icfem09-proof.pdf https://www.umsec.umn.edu/sites/www.umsec.umn.edu/files/hard... LOCK project was pretty landmark in all that it accomplished with Sidewinder firewall & SELinux being in its ripple effects http://www.cyberdefenseagency.com/publications/LOCK-An_Historical_Perspective.pdf http://www.cyberdefenseagency.com/publications/LOCK-An_Histo... The B method is one of most successful in industry. You'll definitely see the engineering aspect in this one. http://www.methode-b.com/wp-content/uploads/sites/7/2012/08/ClearSy-Industrial_Use_of_B1.pdf http://www.methode-b.com/wp-content/uploads/sites/7/2012/08/... Cleanroom was early one in 1980's (start at p13) https://www.sei.cmu.edu/reports/96tr022.pdf https://www.sei.cmu.edu/reports/96tr022.pdf Note: Cleanroom had excellent results at low cost but disappeared for some reason. I saw someone recently combine Python with Cleanroom with good results. Cleanroom's compositional style means something like Haskell + QuickCheck could be great combo. If anyone tries it, let me know about the results.

nickpsecurity 10y ago

Glad you enjoyed it. Remember Praxis' method next time some fool says you can't engineer software. A few companies like them do. They're now just called Altran. The Tokeneer link was good since they published the source code on AdaCore website for people to learn from. However, the highest-security thing they did was the CA below under UK equivalent of EAL6/7. http://www.anthonyhall.org/c_by_c_secure_system.pdf http://www.anthonyhall.org/c_by_c_secure_system.pdf Example of new one for model-to-code-to-ASM verification https://www.umsec.umn.edu/sites/www.umsec.umn.edu/files/hardin-icfem09-proof.pdf https://www.umsec.umn.edu/sites/www.umsec.umn.edu/files/hard... LOCK project was pretty landmark in all that it accomplished with Sidewinder firewall & SELinux being in its ripple effects http://www.cyberdefenseagency.com/publications/LOCK-An_Historical_Perspective.pdf http://www.cyberdefenseagency.com/publications/LOCK-An_Histo... The B method is one of most successful in industry. You'll definitely see the engineering aspect in this one. http://www.methode-b.com/wp-content/uploads/sites/7/2012/08/ClearSy-Industrial_Use_of_B1.pdf http://www.methode-b.com/wp-content/uploads/sites/7/2012/08/... Cleanroom was early one in 1980's (start at p13) https://www.sei.cmu.edu/reports/96tr022.pdf https://www.sei.cmu.edu/reports/96tr022.pdf Note: Cleanroom had excellent results at low cost but disappeared for some reason. I saw someone recently combine Python with Cleanroom with good results. Cleanroom's compositional style means something like Haskell + QuickCheck could be great combo. If anyone tries it, let me know about the results.