[langsec-discuss] Will we ever "solve" security, or prove that we can't?

Tony Arcieri bascule at gmail.com
Thu Jan 19 05:02:45 UTC 2017


On Wed, Jan 18, 2017 at 8:22 PM, Chad Brewbaker <crb002 at 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.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mail.langsec.org/pipermail/langsec-discuss/attachments/20170118/8fc83183/attachment.html>


More information about the langsec-discuss mailing list