2 ms·

> The Apollo program fixed for inflation is something like $130 billion. That's buys you a lot of talent, testing, etc. $130 billion was the total Apollo progr

by n00b101 10y ago

> The Apollo program fixed for inflation is something like $130 billion. That's buys you a lot of talent, testing, etc. $130 billion was the total Apollo program budget. For the Apollo Guidance Computer (AGC) software in question, "In total, software development on the project comprised 1400 person-years of effort, with a peak workforce of 350 people." [1] I would value 1400 programmer person-years at about $200 million. So ... a lot of money, but still less than GitHub's $250 million Series B raise. Edit: Also, refer to the Mythical Man-Month for explanation of why throwing people and money at a software project doesn't guarantee success. > Apollo 1 deaths This was not due to any AGC software bugs. It was a cabin fire during a launch rehearsal test at Cape Canevaral and was essentially a plumbing design issue. [2] > Apollo 11 eating up all the CPU during lunar landing That was not catastrophic and was NOT due to an AGC software bug. It was caused by a peripheral hardware error. In fact AGC software's priority scheduler design actually saved the Apollo 11 mission and crew by recovering the CPU. [3] > Apollo 13's famous O2 tank explosion Again, nothing to do with the AGC software. Apollo 13 was a mechanical failure related to the famous O-ring issue. [4] [1] https://en.wikipedia.org/wiki/Apollo_Guidance_Computer#Software https://en.wikipedia.org/wiki/Apollo_Guidance_Computer#Softw... [2] https://en.wikipedia.org/wiki/Apollo_1#Major_causes_of_accident https://en.wikipedia.org/wiki/Apollo_1#Major_causes_of_accid... [3] https://en.wikipedia.org/wiki/Apollo_Guidance_Computer#PGNCS_trouble https://en.wikipedia.org/wiki/Apollo_Guidance_Computer#PGNCS... [4] https://en.wikipedia.org/wiki/Space_Shuttle_Challenger_disaster https://en.wikipedia.org/wiki/Space_Shuttle_Challenger_disas...

nickpsecurity 10y ago
The cost vs results obtained where astronomical and ridiculous. Ok for such pioneering work hitting many grand challenges at once. Not in any way applicable to normal software development given its constraints. However, I think a few numbers from high and medium assurance are interesting to show how things improved. 1. The high-assurance LOCK program to build secure HW/SW system w/ UNIX compatibility layer cost only 58% more than a normal, solid development. That's with ancient formal methods. 2. Altran/Praxis uses strong requirements gathering, formal specs in Z, language-level safety with Ada, design-by-contract for interfaces, SPARK where possible to prove absence of specific errors, and plenty of testing. Error rate is around 0.04 per Kloc. Cost about 50% extra the one time I heard a price reference. 3. seL4 spent about $350/loc on a 10,000 loc system for formal verification down to C itself. 4. COGENT is one of approaches moving safety into type system of safe, system language with certified translators. This allowed non-experts to safe-code the ext2 file system with effort going down from 1.65 person-months per 100 loc in seL4 to 0.69 in COGENT. So, we're steadily seeing the level and pervasiveness of assurance go up in these projects while cost goes down. Also, as in 80's and 90's recommendations, the best results come from applying high-assurance engineering to stuff that is small, changes little, aids correctness of other stuff, and is reusable. Fortunately, some of our most important stuff has those properties. Including compilers, type systems, parser generators, TLS-style protocols, standard libraries, and so on. So, we certainly can't spend Apollo money on a pile of assembly code using rope memory getting Apollo results. We can spend 30-50 percent on improvements to software development using existing tools to get nearly 0.04 defects per kloc. We can also do better than Apollo using state-of-the-art tooling like Isabelle/HOL, COGENT, QuickCheck, Design-by-Contract, SPARK, and CakeML. Each thing we build, if focusing on right places, can bootstrap more trust or quality into the other stuff. So, given existing and open-sourced work, it's just as exiting time to be in high-assurance engineering as it was back when Hamilton et al had free reign to invent it. [1] https://cryptosmith.files.wordpress.com/2014/10/lock-eff-acmp.pdf https://cryptosmith.files.wordpress.com/2014/10/lock-eff-acm... [2] http://www.anthonyhall.org/c_by_c_secure_system.pdf http://www.anthonyhall.org/c_by_c_secure_system.pdf [3] https://www.semanticscholar.org/paper/From-a-Verified-Kernel-towards-Verified-Systems-Klein/3da1cb0dbeffaf56a2e636032935c24d2e102349/pdf https://www.semanticscholar.org/paper/From-a-Verified-Kernel... [4] https://ts.data61.csiro.au/projects/TS/cogent.pml https://ts.data61.csiro.au/projects/TS/cogent.pml

by n00b101 10y ago

nickpsecurity 10y ago

The cost vs results obtained where astronomical and ridiculous. Ok for such pioneering work hitting many grand challenges at once. Not in any way applicable to normal software development given its constraints. However, I think a few numbers from high and medium assurance are interesting to show how things improved. 1. The high-assurance LOCK program to build secure HW/SW system w/ UNIX compatibility layer cost only 58% more than a normal, solid development. That's with ancient formal methods. 2. Altran/Praxis uses strong requirements gathering, formal specs in Z, language-level safety with Ada, design-by-contract for interfaces, SPARK where possible to prove absence of specific errors, and plenty of testing. Error rate is around 0.04 per Kloc. Cost about 50% extra the one time I heard a price reference. 3. seL4 spent about $350/loc on a 10,000 loc system for formal verification down to C itself. 4. COGENT is one of approaches moving safety into type system of safe, system language with certified translators. This allowed non-experts to safe-code the ext2 file system with effort going down from 1.65 person-months per 100 loc in seL4 to 0.69 in COGENT. So, we're steadily seeing the level and pervasiveness of assurance go up in these projects while cost goes down. Also, as in 80's and 90's recommendations, the best results come from applying high-assurance engineering to stuff that is small, changes little, aids correctness of other stuff, and is reusable. Fortunately, some of our most important stuff has those properties. Including compilers, type systems, parser generators, TLS-style protocols, standard libraries, and so on. So, we certainly can't spend Apollo money on a pile of assembly code using rope memory getting Apollo results. We can spend 30-50 percent on improvements to software development using existing tools to get nearly 0.04 defects per kloc. We can also do better than Apollo using state-of-the-art tooling like Isabelle/HOL, COGENT, QuickCheck, Design-by-Contract, SPARK, and CakeML. Each thing we build, if focusing on right places, can bootstrap more trust or quality into the other stuff. So, given existing and open-sourced work, it's just as exiting time to be in high-assurance engineering as it was back when Hamilton et al had free reign to invent it. [1] https://cryptosmith.files.wordpress.com/2014/10/lock-eff-acmp.pdf https://cryptosmith.files.wordpress.com/2014/10/lock-eff-acm... [2] http://www.anthonyhall.org/c_by_c_secure_system.pdf http://www.anthonyhall.org/c_by_c_secure_system.pdf [3] https://www.semanticscholar.org/paper/From-a-Verified-Kernel-towards-Verified-Systems-Klein/3da1cb0dbeffaf56a2e636032935c24d2e102349/pdf https://www.semanticscholar.org/paper/From-a-Verified-Kernel... [4] https://ts.data61.csiro.au/projects/TS/cogent.pml https://ts.data61.csiro.au/projects/TS/cogent.pml