4 ms·

Here's my hypothesis: The problem with these static verifiers is that they are applied at the wrong stage. The verification logic would be more useful in more c

Here's my hypothesis: The problem with these static verifiers is that they are applied at the wrong stage. The verification logic would be more useful in more cases if it were applied at the optimization stage. Right now the benefits of static verifiers is rather binary. Either your program (or code unit) is sucessfully verified or it isn't. And every time you make a change to verified code you risk losing its verified status. Imagine instead writing code that is made "safe" using run-time asserts everywhere. Unoptimized, this code might be slow. And unreliable in the sense that a run-time assert could fail, requiring some kind of recovery or abort action. But it would still be "safe". The run-time asserts are effectively the "program specifications", and the discarding of those asserts at the optimization stage is basically equivalent to traditional static verification. The difference being that not quite fully optimized "safe" code is generally more valuable than not quite fully verified (and therefore not fully "safe") code. > These heady days of being able to deny responsibility and shove out any software we want without consequence need to end. If the static verification community is imploring the development community to, with some effort, change its practices to improve code safety, would that community be willing to, with some effort, move the application of their verification logic to the optimization stage where it would be more practical for a wider range of applications?

KirinDave 9y ago
> Here's my hypothesis: The problem with these static verifiers is that they are applied at the wrong stage. They can be applied at lots of stages. Why not apply them to all of them? > Either your program (or code unit) is sucessfully verified or it isn't. This is demonstrably false. It can help you write better, safer code incrementally. Every approach that is discussed here has a "refinement" plan. > Imagine instead writing code that is made "safe" using run-time asserts everywhere. I can imagine this, it's the C/C++ style of code circa 2010. It's awful for users. But it's not what we're discussing here. > If the static verification community is imploring the development community to, with some effort, change its practices to improve code safety, would that community be willing to, with some effort, move the application of their verification logic to the optimization stage where it would be more practical for a wider range of applications? Yes. You're already seeing two major examples of this: Type Providers and derivations of dependent types fall into one camp, dependent type implementations (of which the most prominent is Idris) fall into the other. All of them offer the ability to extend the type system and make proofs useful to developers even as they also help make code total and enforcible. I think it's further along than you seem to suggest. Can I suggest you grab a copy of Atom, Atom-Idris, and go through some Idris tutorials? You can also try F# and use Json samples pulled from an API to generate types that inform your tooling and improve code quality.
nickpsecurity 9y ago
As KirinDave said, we can apply our tech to as many stages as we like. If applied redundantly, has the extra benefit of verification at one stage catching problems in an earlier one. Far as propagating verification conditions or checking in middle, you might find these concerns addressed by proof-carrying code plus equivalence checks on untrusted optimizations as in VeLLVM. There's also work that equivalence checks transformations in assembly code. https://news.ycombinator.com/item?id=16041110 https://news.ycombinator.com/item?id=16041110

KirinDave 9y ago

> Here's my hypothesis: The problem with these static verifiers is that they are applied at the wrong stage. They can be applied at lots of stages. Why not apply them to all of them? > Either your program (or code unit) is sucessfully verified or it isn't. This is demonstrably false. It can help you write better, safer code incrementally. Every approach that is discussed here has a "refinement" plan. > Imagine instead writing code that is made "safe" using run-time asserts everywhere. I can imagine this, it's the C/C++ style of code circa 2010. It's awful for users. But it's not what we're discussing here. > If the static verification community is imploring the development community to, with some effort, change its practices to improve code safety, would that community be willing to, with some effort, move the application of their verification logic to the optimization stage where it would be more practical for a wider range of applications? Yes. You're already seeing two major examples of this: Type Providers and derivations of dependent types fall into one camp, dependent type implementations (of which the most prominent is Idris) fall into the other. All of them offer the ability to extend the type system and make proofs useful to developers even as they also help make code total and enforcible. I think it's further along than you seem to suggest. Can I suggest you grab a copy of Atom, Atom-Idris, and go through some Idris tutorials? You can also try F# and use Json samples pulled from an API to generate types that inform your tooling and improve code quality.

nickpsecurity 9y ago

As KirinDave said, we can apply our tech to as many stages as we like. If applied redundantly, has the extra benefit of verification at one stage catching problems in an earlier one. Far as propagating verification conditions or checking in middle, you might find these concerns addressed by proof-carrying code plus equivalence checks on untrusted optimizations as in VeLLVM. There's also work that equivalence checks transformations in assembly code. https://news.ycombinator.com/item?id=16041110 https://news.ycombinator.com/item?id=16041110