3 ms·
I see it is implemented in C. Doesn't this add a substantial attack surface, especially relevant for web services? How is the "memory-safe" claim justified?
by OutOfHere 2y ago
I see it is implemented in C. Doesn't this add a substantial attack surface, especially relevant for web services? How is the "memory-safe" claim justified?
- burnt-resistor 2y agoThere is a pervasive, cultural lack of formal verification in software, and it's risky, terrible, and should be stopped. Formal verification can takes multiple forms and operates at different spans across the layers of the stack. We need more of it to prove the correctness of compilers, libraries, and programs. It is a lot of work, but it's critical to proving things are as good, as say, seL4.
- johnisgood 2y agoWe need more Ada / SPARK!
- tlarkworthy 2y agothere is a culture of type safety which is a very watered down machine checked proof that the thing entering a function has affordances X,Y and Z. Its not the end to end functional verification you are talking about but its not nothing either.
- up2isomorphism 2y agoYes, it opens a large attack surface for a group of people who thinks “memory-safe” is only possible when that word appears on the top of a language’s features list.