5
$\begingroup$

There are standard courses in computer science faculties that teach software verification, yet modern software products (Operating Systems especially) require periodic updates and bugs are constantly found. Windows code is so complex, I don't have an idea how one would verify its correctness, it seems that testing instead of verification is state of art in modern software engineering products and that's why we require testers. Does software verification have any usage in near future to help us to verify correctness of modern software products, especially ones that are widely used?

$\endgroup$
8

4 Answers 4

9
$\begingroup$

This is actually a surprisingly complex topic.

Who verifies the verifiers?

Have you heard of Ada/SPARK?

Ada is a programming language which is mostly used in embedded contexts, including in military contexts. SPARK is an "add-on" for Ada, which lets one specifies invariants, pre-conditions, and post-conditions, and will check that those are met at compilation time.

This means that we have a (somewhat) mainstream language with built-in verification.

The standard library is itself verified with SPARK, for example, the sort method is verified to sort... or well, now it's verified. Hopefully.

A few years ago, someone realized that the post-condition of sort was insufficient: it just specified that the output must be sorted. The author then went through quite a few tries attempting to find the correct specification, it went something like this:

  1. Post-condition: sorted. [] is a valid output for all inputs...
  2. Post-condition: sorted and of same length. [0, ...] is a valid output for all inputs.
  3. Post-condition: sorted, of same length, and all elements are from input. [input[0], input[0], ...] is a valid output for all inputs.

Finally, the author realized that the correct specification was to require that the output be both sorted and a permutation of the input.

Whether automated proofs, or human-derived proofs, just ensuring that the software as written follows the specification is not good enough: the specification can simply be wrong, or insufficiently precise.

Complexity

Modern software is big. Mind-boggingly big. Windows has dozens of millions of lines of code.

Modern software is concurrent. Meaning that race-conditions are expected, and both pre-conditions, invariants, and post-conditions must account for them.

Modern software runs on fallible hardware. ECC RAM is not mainstream, disks regularly fail, CPU overheat, etc...

Yet, there is hope

Ada/SPARK is merely the most well-known example I could think of. We could also talk about Eiffel (Design by Contract) or C++ (thinking about adding contracts) or Rust and its cohort of SPARK-like plugins such as Creusot.

There are also more lightweight alternatives. In Rust, for example, the Kani crate allows writing symbolic tests.

And there are out-of-the-box ideas as well. The Cranelift compiler, for example, features symbolic translation verification. Formally proving a compiler is a Sisyphean task -- after over a decade, CompCert has only a handful of verified optimizations -- so instead of one the Cranelift developer had an idea: if we can't prove that a transformation pass will preserve semantics in all cases, could we prove that for the case at hand semantics were preserved? And the answer is yes! The Cranelift compiler comes with the option to do so. The cost is relatively modest (~2x compilation time), and in exchange you have a quasi-assurance that the transformation was correct -- or a compiler error.

The latter example -- Cranelift -- is actually particularly interesting because it demonstrates both:

  1. That there is interest from industry stakeholders to invest in verification.
  2. That even complex applications such as compilers can benefit from verification.

Perhaps not full-blown, ahead-of-time, formal verification -- though that's also planned for some parts of Cranelift -- due to cost reasons, but automated symbolic verification can be surprisingly affordable, and definitely raises the bar compared to pure testing already.

But, really?

I would not expect formal verification to become part and parcel of mainstream software development any time soon.

The rising level of threats is tipping the balance though. The fact that the US agencies recently published a white-paper recommending the use of memory-safe languages, or that both Linux and Windows have started on the integration of Rust, is a sign that consciousness are evolving in response to those threats.

I expect, thus, that the use of verification -- in some form -- will become more and more prevalent in critical software. It will take time, though, and the use of formal verification will likely remain confined to high-value low-complexity targets, for cost reasons.

$\endgroup$
9
  • $\begingroup$ I agree. There is definite industry interest, but the task is monumental. Microsoft didn't hire Tony Hoare for nothing. MS Research spends a significant amount of time and money on safety-related aspects of all shapes and sizes, including formal verification. And that's just what I am familiar with from watching old videos of Erik Meijer interviewing his colleagues. I am sure other OS and platform vendors (IBM, Oracle, Google, Amazon) as well as "vendors" like Linux (via companies like RedHat and Canonical as well as contributions from universities) are in the game as well. $\endgroup$ Apr 2 at 13:06
  • 1
    $\begingroup$ In addition of the specification being simply "wrong", ("too coarse" as in your example) your specification may also include requirements that are too restrictive. They make sense as you start developing your program, but as the program expands, they become a hindrance, preventing the program from exhibiting newly desired behaviour. How do you relax such requirements in the development process, without losing the guarantees given by formal verification formerly based on the strict requirement - as it would open the door to regression? $\endgroup$ Apr 3 at 13:17
  • 1
    $\begingroup$ @LaurentLARIZZA: Good point. Loosening the pre-conditions is typically not an issue, loosening the invariants or post-conditions requires redoing the analysis of all downstream... which is costly, when manual. This where the advantages of automated provers shine. $\endgroup$ Apr 3 at 14:55
  • 1
    $\begingroup$ @reinierpost: I certainly did not wish to imply that contracts were new (Eiffel is from 1985). Many languages without contracts have informal equivalents (assert constructs, for example). The problem with run-time verification, of course, is that while you may not get the wrong answer, you may crash the system. And god forbid accidental side-effects in assert-like constructs when those can be disabled in production... I do like contracts/asserts, but they're not without downsides, even before considering run-time costs and development costs. $\endgroup$ Apr 3 at 15:00
  • 1
    $\begingroup$ Code Contracts for .NET supported static verification. $\endgroup$ Apr 4 at 13:02
4
$\begingroup$

To be honest this feels like it's a question of just practicality and feasibility. The reality is that all of our systems are just so complex these days, that it's almost impossible to just verify that everything is correct without testing.

You can write code that is theoretically 100% correct, and still run into issues based on how it's run, or what sort of engine or processor you're using. An easy example would be coding for websites, or using any of the newer popular Javascript libraries out there.

I have a website with some animations where the animation follows your mouse pointer. If you run the animation on Chrome it works 100% as expected without any issues. However, when you switch to Firefox, the animations don't work the same way, and don't work as good. The APIs used to make the animation work are the same regardless of browser used, however, the way the API behaves on Firefox is slightly different from how it works on Chrome.

Issues like these are bound to arrise, and when you get to something like Operating Systems, it's the same situation, there are hundreds of different CPUs out there all potentailly working slightly differently. Also different compilers which will give you a different assembly output for the same piece of C/C++ code. They've also made Windows for ARM CPUs, which would require quite a large re-write of certain areas of code. The fact that a different CPU is being used, means that, although the operating system might feel like it's the exact same, the way it works on the inside must be changed by quite a bit for it to work on an ARM.

It just makes it almost impossible to verify correctness of a piece of code, as at the end of the day, you can write the code perfectly correct. But it can still run into issues just by changing browser or CPU.

This actually even applies for algorithms. Currently, we do not have any systems that autonomously verifies the correctness of your algorithm, and as far as I know it's actually impossible in certain cases (there's probs a good proof for this, but, if you could on the fly verify correctness of all algorithms, without running it, you would most likely have solved the P equals NP problem). It's also just super easy to generate a set of 100 thousand test cases with answers, and compare your solution to the test cases. (Which is what all the competitive programming websites like Leetcode do)

But then again, even on my website, the animations actually look okay on Firefox. They just don't feel as good as it does on Chrome. So it's actually okay to have a bug or two sometimes, no one said everything has to be perfect. So practically it's just easier to have test-units, and sometimes guess-and-check, than it is to be 100% certain that something is 100% correctly written.

TL;DR, it's just impossible to 100% certainly verify correctness for probably most cases. Meanwhile testing is super easy to do, and a few bugs are basically just always expected to be in a large codebase.

$\endgroup$
2
  • 1
    $\begingroup$ thank you for the answer, Yeah, hard part is that for verification, we also need to know specifications of our machine(CPU, memory etc.) then compiler and language as well, basically we have to know every level of abstraction in detail to 100% verify something. $\endgroup$
    – math boy
    Apr 2 at 18:41
  • 2
    $\begingroup$ Re: "if you could on the fly verify correctness of all algorithms, without running it, you would most likely have solved the P equals NP problem": Heck, it's worse than that: according to Rice's theorem, this would solve the halting problem, which is known to be undecidable. $\endgroup$
    – ruakh
    Apr 2 at 21:35
0
$\begingroup$

I've worked as a software API tester for over 20 years and I often wanted to apply more formal methods for verifying correctness but found that timelines are too short to do it properly.

I suspect that this can at least be somewhat integrated into static code analysis tools or into the compiler itself using some kind of model checking method.

$\endgroup$
1
  • $\begingroup$ thank you for providing personal experience, I consider this answer short and not detailed enough to upvote it. $\endgroup$
    – math boy
    Apr 5 at 23:27
-2
$\begingroup$

Let's shed some light on where and how software verification is used(apart from widely used software). Have a look at this.

Space, Military, Telecom, Finance and more. These are the fields where software bugs have caused significant problems. But how did these bugs arise in the first place? Was the development process so lax? It doesn't seem likely, given the criticality of those domains. There could be hardware components that could have failed. How come a logical entity failing be just as harmful as a physical entity failing?

Answers to questions like these can be summarised as

  1. Hardware components are bound by the laws of physics and they would definitely fail. Hence we have statistical models of reliability which help us take preventive and corrective measures to ensure that the component performs as expected during it's lifetime. This isn't the case with software.
  2. The state space of a software, would practically be too large to be tested thoroughly. Furthermore, testing shows the presence of bugs, not it's absence.
  3. It isn't always possible to test the end product(ex: safety codes for nuclear reactors, software for avionics systems etc)
  4. Updating/Maintenance of software/hardware needs to ensure it doesn't break anything that was previously working.

Having a mathematical proof of software/program correctness suddenly seems lucrative. But as far as mathematics goes(and so do the other answers here), verification is an undecidable problem.

But it, in no way stops engineers and scientists to cirumvent around and find ways, to somehow, although partially, get closer to the idea of a program being correct. This includes things like using a restricted subset and programming guidelines(JPL power of 10, MISRA C) for development and verification through tools like Model checking, Abstract Interpretation and more.


software should be assumed to be faulty until application of the currently accepted best practice methods can demonstrate that it is correct.

Courtesy: Arianne 5 failure analysis

$\endgroup$
2
  • 1
    $\begingroup$ I don't see how this answers the question. It contains some interesting discussion on the general topic area that the question falls into, and it proposes some alternative questions and answers to those alternative questions, but I don't see a direct answer to the specific question that was asked. As a reminder, the question was "Does software verification have any usage in near future to help us to verify correctness of modern software products, especially ones that are widely used?" $\endgroup$
    – D.W.
    Apr 3 at 17:22
  • $\begingroup$ I think it provides some interesting insights, so I won't downvote the answer, however it doesn't provide ideas about the exact question that was asked as mentioned by @D.W , so I won't upvote it. $\endgroup$
    – math boy
    Apr 5 at 23:22

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.