4 ms·

I believe that formal verification is the next big thing. The problem with software reliability and security becoming the most critical one and this is the way

I believe that formal verification is the next big thing. The problem with software reliability and security becoming the most critical one and this is the way to tackle it. There is sufficient research in academia which could be used as a foundation to build tools for the industry.

tester756 5y ago
but is formal verification required/needed to solve latest security issues? I mean those related to: CPUs, NPM, External Libraries, parsers written in unsafe languages
- vzaliva 5y ago
  In short: Yes. In many cases having solid formal foundation allows to fomulate high-level properties which would allow to catch even bugs like recent log4j. There is alreay a lot of work on formalization of ISA/CPU definitions which could allow to catch low-level bugs/expoloits.
  - tjansen 5y ago
    "catch even bugs like recent log4j" How could it help with that? JNDI lookups were a documented feature of log4j. An incredibly dangerous one, but it was intended to work like that.
    - AnimalMuppet 5y ago
      Well... it might have raised a red flag about how incredibly dangerous the feature was, because there would be no way to make the verification shut up about the code that implemented the feature (if the verification did a good job). I don't know about log4j, but in the case of many such features, there would be a PM or somebody insisting that you have to implement his pet idea, no matter how much the tool screams.
    - vzaliva 5y ago
      One can define a high-level security property, like "not executing remotely-downloaded code" and try to prove that no execution path of the program triggered by input data violates it. The formal verification will force you to consider all possible scenarios to be able to prove that this is not going to happen.