28 ms·

The marketing for FV is indeed rare in larger software industry, probably because of quite small susceptible market. The latter is small, because 1) the FV proc

The marketing for FV is indeed rare in larger software industry, probably because of quite small susceptible market. The latter is small, because 1) the FV process is expensive 2) it gives only limited benefits. Most of the marketing that exists for FV in software is done by academia and few MIC companies like Greenhills Software or General Dynamics. In practice almost nobody in software produces formally verified software. And when they do, like the few examples that exist, the proof only guarrantees what design could foresee, and only if assumptions are satisfied which is not trivial in real deployments. It may work for avionics on special isolated simple hardware, but cloud hosted VMs on x86/ARM connected to Internet is probably too far.

naasking 5y ago
> And when they do, like the few examples that exist, the proof only guarrantees what design could foresee, and only if assumptions are satisfied which is not trivial in real deployments. In other words, formal verification can: 1. provide guarantees that the implementation matches the spec, 2. that the spec fulfills certain properties, including but not limited to security, safety, reliability properties These are typically more guarantees that non-verified software, so I still fail to see how this is bullshit marketing. In this case, they proved that there are no overt information flow vulnerabilities in the design or implementation, so you're left only with the covert channels. That's clearly a valuable property to know. If Intel, AMD or RISC-V releases a covert-channel free CPU, then you can even close those and it's secure from top to bottom.
- posix_me_less 5y ago
  Yes but the spec is often unknown (C language, GCC compiler, Linux) or flawed (speculative execution processors, which we know since Spectre). The fact there is a formally verified piece of design and software is not bullshit. I said the marketing here is bullshit. This shiny piece of great software won't solve our security problems in multiuser environments, because the proof works only under a very limited set of assumptions. You can't just run your VMs in the cloud on this FV hypervisor and think your software security problems are solved.

naasking 5y ago

> And when they do, like the few examples that exist, the proof only guarrantees what design could foresee, and only if assumptions are satisfied which is not trivial in real deployments. In other words, formal verification can: 1. provide guarantees that the implementation matches the spec, 2. that the spec fulfills certain properties, including but not limited to security, safety, reliability properties These are typically more guarantees that non-verified software, so I still fail to see how this is bullshit marketing. In this case, they proved that there are no overt information flow vulnerabilities in the design or implementation, so you're left only with the covert channels. That's clearly a valuable property to know. If Intel, AMD or RISC-V releases a covert-channel free CPU, then you can even close those and it's secure from top to bottom.

posix_me_less 5y ago
Yes but the spec is often unknown (C language, GCC compiler, Linux) or flawed (speculative execution processors, which we know since Spectre). The fact there is a formally verified piece of design and software is not bullshit. I said the marketing here is bullshit. This shiny piece of great software won't solve our security problems in multiuser environments, because the proof works only under a very limited set of assumptions. You can't just run your VMs in the cloud on this FV hypervisor and think your software security problems are solved.