logoalt Hacker News

nickpsecurity • yesterday at 9:23 PM • 1 reply • view on HN

The math can be misinterpreted, misapplied, or not fit reality. That's why high-assurance security mandated a combination of things:

1. English specification of the system and its goals

2. Formal, mathematical specification of the system and its goals

3. Mathematical proof the system met its goals

4. Code implementing that system with a proof, often informal, that the code embodied the informal and formal design.

5. Tests of all functionality to prove the design and code worked.

6. Independent analysis of the above to find flaws in them.

7. If the implementation has concurrency or parallelism, more errors can occur due to that. There were techniques to mitigate it.

Each step found problems in systems made by professionals. Mathematical work and coding both have a long history of errors in their on fields. Combining them increases the likelihood of error.


Replies

kooi • yesterday at 9:42 PM

Not sure what all these words mean. These are mathematical results, I'm not sure why people are acting like they are anything otherwise.

➕ show 1 reply