4 ms·

> "Machine checked formally verified" is a long-known buzzword that screams bullshit marketing. Long-known to who, exactly? How is "formal verification" even r

> "Machine checked formally verified" is a long-known buzzword that screams bullshit marketing. Long-known to who, exactly? How is "formal verification" even remotely a marketing buzzword?

posix_me_less 5y ago
To people interested in software process. There is a consensus that formal verification and automatic checks in software (even hardware) are a debugging tool, not a comprehensive success/security policy like the linked article would suggest.
- cvwright 5y ago
  "People interested in software process" have been trying, and failing, to write secure C code for 50 years. But they've made a ton of money trying!
  - posix_me_less 5y ago
    C was not initially intended for such a thing, although later people tried to restrict it. Also, "secure C code" is too vague. It depends on the scope. Grep is quite secure in what it does. Linux, less so.
- touisteur 5y ago
  I'm curious where you get this consensus. It's not at all shared by everyone, especially with the huge strides SPARK and Frama-C have made.
  - posix_me_less 5y ago
    I didn't mean academic consensus. More like industry / security-aware people in IT consensus - almost nobody in software does formal verification and it would be foolish for any user, whether person, business or government, to take this as solution to their VM hosting security problems. Yes formal verification has made advancements and is a useful tool, in proper context. Not in the context the article is selling the work of the researchers.
naasking 5y ago
I was thinking the same thing. I've never seen "formally verified" used in marketing because almost nobody is willing to put in the money and effort to formally verify software. The only places I've seen it done is when security and reliability is essential to critical operations, like the seL4 kernel.
- posix_me_less 5y ago
  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.

> "Machine checked formally verified" is a long-known buzzword that screams bullshit marketing. Long-known to who, exactly? How is "formal verification" even remotely a marketing buzzword?

posix_me_less 5y ago

To people interested in software process. There is a consensus that formal verification and automatic checks in software (even hardware) are a debugging tool, not a comprehensive success/security policy like the linked article would suggest.

cvwright 5y ago
"People interested in software process" have been trying, and failing, to write secure C code for 50 years. But they've made a ton of money trying!
- posix_me_less 5y ago
  C was not initially intended for such a thing, although later people tried to restrict it. Also, "secure C code" is too vague. It depends on the scope. Grep is quite secure in what it does. Linux, less so.
touisteur 5y ago
I'm curious where you get this consensus. It's not at all shared by everyone, especially with the huge strides SPARK and Frama-C have made.
- posix_me_less 5y ago
  I didn't mean academic consensus. More like industry / security-aware people in IT consensus - almost nobody in software does formal verification and it would be foolish for any user, whether person, business or government, to take this as solution to their VM hosting security problems. Yes formal verification has made advancements and is a useful tool, in proper context. Not in the context the article is selling the work of the researchers.

naasking 5y ago

I was thinking the same thing. I've never seen "formally verified" used in marketing because almost nobody is willing to put in the money and effort to formally verify software. The only places I've seen it done is when security and reliability is essential to critical operations, like the seL4 kernel.

posix_me_less 5y ago
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.