On Wed, Jan 18, 2017 at 8:22 PM, Chad Brewbaker <crb...@gmail.com> wrote:
> Defenders have 100% knowledge of their verification coverage. They can put > a SMT solver in their continuous integration pipeline and flag all code not > verified for removal. > I think you have just described a CI pipeline that's impossible to get any "real world code" through. In the real world people need to "get shit done", and speaking as someone who is presently working with formally verified codebases and who has worked with equivalence verification using SAT/SMT solvers in the past, if what you're describing is the bar, I hope the programmers are also intelligent computers, because if they're humans your company isn't going to get anything done. Have you ever thrown anything remotely complex at a SAT/SMT solver? Have you seen them hit some sort of combinatorial explosion and blow up, hung for a relative eternity in some sort of Turing tar pit? For that matter, have you ever wasted time clearing stuck jobs from a CI pipeline? (Or seen a formally verified CI system? The answers to all these questions are, rhetorically: NOPE) SAT/SMT solvers, in their current form, are relegated to highly constrained and bounded problems, certainly not the sort of, for lack of a better term, "real world code" that holds the world together. Restraint in only shipping verified code is the silver bullet. > Again, in the real world, getting people to even adopt static typing is a huge burden (I say this as someone who works at a company which uses static typing across the board, except for 3rd party SDKs and JavaScript in browsers, unless we're writing TypeScript, PureScript, or Elm), and there's no right vs wrong answer in the dynamic vs static typing debate either. Should someone who's spending late nights to cobble together a barely working demo be forced to shove their code through a SAT solver before the demo is greenlighted? Clearly not, the *business* bounds on their use case in the form of time-limited opportunities would make it completely impractical. It's easy to imagine some sort of fantasy world where everyone understands formal methods and only writes perfect, formally-verified code. But in the real world humans have a widely varying range of skills (which is a *good* thing), problems are ugly, and formal verification doesn't and can't help. I can only hope that over time we see a gradual trend towards a more formal, rigorous approach, but at the same time there are real-world constraints, both practical and computational, which I think will keep the dream of "formally verified software everywhere" down for quite some time.
_______________________________________________ langsec-discuss mailing list langsec-discuss@mail.langsec.org https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss
