Forem: Ahmed Al-Obaidi

Developing critical software: Intro to formal methods and theorem provers

Ahmed Al-Obaidi — Wed, 27 May 2020 15:48:35 +0000

The amount and complexity of software developed and used has grown tremendously. There are many applications where high reliability must be ensured, because failures are costly (with respect to human lives, environmental issues, or money).
There are more safety-critical software systems than you realize, but they don’t get nearly as much attention as consumer-focused software, and it can be found in almost all areas, e.g., aviation, (nuclear) power plants, medicine, transportation, space technologies, process control, and banking.
Whereas the crash of a word processor or your favorite game may be a nuisance, a malfunction in software controlling a nuclear plant could possibly cost thousands of human lives, and could put millions more at risk; recent actual examples of critical systems failing would be Boeing’s 737 MAX groundings, and the “Meltdown and Spectre” Vulnerabilities.

Safety first

In most companies, software developers are primarily concerned with shipping more features, and delivering more value. But software developers involved in the creation of safety-critical systems must be concerned primarily with creating safe systems. And that is a very different task.
Most safety-critical software appears to be developed using the waterfall or spiral models. NASA specifically recommends against using Agile methods for the safety-critical components in its software guidebook (page 87)

Defects per thousand lines of code vs. dependability of multiple systems, the goal here is to show how "different" critical systems are

The problem with testing:

The most common way to check for faults and bugs is to use testing, and human review. During and after the implementation of the system, the system’s functionality is usually tested to ensure that the resulting program satisfies the requirements and that no errors or bugs are present. Testing large and complex systems can be very time consuming and, due to the size of the system and the amount of code, an exhaustive testing is practically impossible. Nevertheless, when the system is safety and security critical, correct functionality must be guaranteed, which requires either exhaustive testing or a way of proving that the code correctly implements the specification.

Formal methods:

In computer science, formal methods are mathematically rigorous techniques and tools for the specification, design and verification of software and hardware Systems. Mathematically rigorous means that the specification consists of Well-formed statements using mathematical logic and that a formal verification consists of rigorous deductions in that logic. A formal specification is precise and there is no risk of misinterpretations. Also, if there is a proof that the implementation abides by the specification, then one can be sure that the programmers have implemented what is described in the specification, which means complete verification of the entire state space of the system.

A basic banking system specification using the "Z" formal specification language

When formal methods cannot be used through the entire development process (due to the complexity of the system, lack of tools or other reasons), they can still be used successfully on parts of the system, for example on the most safety or security critical components alone.

Formal methods are used in several ways:

To assure the software after-the-fact.
To assure the software in parallel.
To develop the software.

“After the fact” software verification can increase the confidence in a safety-critical system. When the regular software development is completed, then the formal specification and verification begin. The software assurance engineer converts the “human readable” requirements into a formal specification and proves properties about the specification. The code that implements the system may also be formally verified in order to comply with the formal specification. With this approach, two separate development activities occur, increasing costs and schedule length. In addition, problems found at this late stage are costly to fix.

“In parallel” software verification still uses two separate teams (software development and FM verification), but they operate in parallel during the whole process. The development team uses the regular practices of good software development. At the same time the FM team writes and verifies the formal system specifications. While still costly, this method of assuring the software allows for quicker development. Software errors are detected earlier in the development cycle when they are less expensive to correct. However, communication between the two teams is crucial for this approach to work.

Instead of having two teams working in parallel, the software can be developed using FM exclusively. This is an integrated approach. Requirements and design are written in a formal language. The design is formally verified before code is generated. This method is the least costly of the three, though the developers must be trained in FM for it to work.

Most formal methods are considered to be too clumsy and time-consuming in their application. They usually require a long learning curve for the software engineer and are often incompatible with the "as-we-always-did" software development procedures. Together with schedules, which are generally very tight, an application of formal methods in an industrial environment is often not accepted by the project team. This is where theorem provers can help.

Interactive theorem provers

By interactive theorem proving, we mean some arrangement where the machine and a human user work together interactively to produce a formal proof. There is a wide spectrum of possibilities. At one extreme, the computer may act merely as a checker on a detailed formal proof produced by a human; at the other the prover may be highly automated and powerful, while nevertheless being subject to some degree of human guidance.
ITPs can be customized to specific application domains by providing
libraries of tactics, thus increasing the amount of automatic processing.
On the other hand, interactive theorem provers have several serious disadvantages:

they can sometimes become “too interactive”, Even the smallest steps in the proof must be carried out by hand.
Large and complicated proofs take weeks to months to be completed.
most interactive theorem provers can only be used by people who have a lot of knowledge and experience in the application domain, the calculus, and sometimes even the implementation language of the prover, Therefore, the use of interactive theorem provers requires specially trained and experienced people.

Isabelle, an interactive theorem prover

Automated theorem provers

Automated theorem provers are programs which, given a formula, try to evaluate whether the formula is universally valid. Currently, most ATPs are like racing cars: although very fast and powerful, they can’t be used for everyday traffic, because essential things (like headlights) are missing. The classical architecture of ATPs must be extended to several directions in order to be useful for real applications.
Automated theorem provers are not a universal cure for every application and every proof obligation, even if they could be processed by the prover; In many cases, user interactions will always be necessary to perform complex core proof operations, However, the goal is to relieve the user from tedious low-level detail-work. Ideally, automated theorem provers can play a role in software engineering equivalent to a pocket calculator in classical engineering: simple tasks are done automatically, but there is still work to be done by the engineer.
Another problem with automated theorem provers is that, in most cases, there is no user interface, and no possibility of debugging a formula. Current implementations expect a syntactically correct formula, and they provide no feedback if no proof can be found.

The theorem prover museum is an initiative to conserve the sources of theorem prover systems for future analysis, since they are important scientific artifacts. It has the sources of many of the theorem provers.

examples of practical use:

Formal methods have been successfully used on NASA, military, and commercial systems that were considered safety-critical applications, and interactive theorem provers such as Isabelle are being used successfully in verification of compilers, protocols, hardware, and algorithms.

The seL4 micro-kernel has been formally verified from its abstract specification down to its C implementation using machine checking. The correctness of a very detailed, low-level design is shown, and the C implementation is formally verified.
An abstract specification of the system was created as an operational model of the system. Then the Haskell programming language was used to implement a prototype of the kernel. This prototype could be automatically translated into the theorem prover Isabelle to form an executable, design-level specification of the kernel. Then the mode was manually implemented in C to form a high-performance C implementation of seL4.
AMD, Intel and others use automated theorem proving to verify that division and other operations are correctly implemented in their processors.
Lightweight Java programming language was designed for academic purposes within the Computer Laboratory of university of Cambridge. it was proven type-sound using Isabelle.

Sources

J. Schumann, Automated Theorem Proving in Software Engineering, Springer, 2001

I. Rodhe, M. Karresand, Overview of formal methods in software engineering, 2015

J. Harrison, J. Urban, F. Wiedijk, History Of Interactive Theorem Proving

NASA Software Safety Guidebook

B. Osepchuk, Safety-Critical Software: 15 things every developer should know, 2020

Retaining what you learn, and developing your mental models (feat. Anki)

Ahmed Al-Obaidi — Sat, 22 Feb 2020 23:56:43 +0000

This post mainly targets software developers; however, the practices presented are already being applied with success by medical students, and people learning new languages as well.

The problem:

When I first started learning software development fundamentals a few years ago, I used to learn so much by simply reading or watching anything related to software development, and what made me learn even more is the fact that I’m a person who likes digging holes, if an article mentions a concept that I don’t know, I would go and find another article that explains that concept, but that blog post introduces yet another concept and I have to find out about that, and so on and so forth until I have 17 tabs open and I don’t remember where I came from anymore; during that period, I was focusing on broadening my knowledge; I felt bad because I knew I won’t be able to retain all this as I wasn’t necessary going to regularly use all of it anytime soon.

The solution:

I started using Anki; it's basically a flashcards program, you simply create cards, and the program will handle the rest, it knows when you should review each card to successfully retain the information on that specific card, it's based on active recalling, and spaced repetition; 2 years ago I wasn't sure about this whole Anki thing, but I decided to give it a shot anyway, today I can say with confidence that it does work, but don't just take my word for it, I highly recommend that you read Anki's own introduction, and Gwern Branwen's excellent article about spaced repetition these two are more important than this post, read them if you have the time.
I won't be exploring the program itself, it's relatively straight forward, and there are many great articles and videos out there that explain how to use it.

Johann Gutenberg, by Granger

When I'm reading a book, I highlight the parts that I think are important, and after I'm done reading, I start creating Anki cards for the highlighted parts, I try my best to write "good" cards for each highlighted part, this is the trickiest and the most important part, things that I avoid are:

Questions related to language syntax.
Questions that only require remembering what a specific method does.
Questions like this one: “Lessons learned from chapter 2”.
Creating cards with long answers; it's better to break them down to multiple smaller cards.
Writing sketchy answers: only writing the keywords in the answer, or using sentences like "refer to page x" or "read article y"; this is bad because you not only want to answer the questions, but you also want to answer them the same way every time, and having to go through an article every time isn't exactly going to help you do that; it's also bad because you're assuming that you'll have access to the book or the article that you're referring to when doing your cards, which isn't always true, in my case for example, I tend to do my cards using my phone when commuting to work.

What I do is that I write questions that help me develop my mental model for the topic I'm reading about, these are usually "why?" questions, I found this type of questions to be by far, the most effective; I also found that if there's an important part, and that part that has a diagram for it, then I can simply take a screenshot and use that diagram as the answer.

Sometimes I find that there's an important part that I just can't convert to a flashcard format, in that case, I use “cloze cards”, they're simply fill-in-the-blank questions; I use this type sparingly as I always try to create regular cards instead.

When you first start using Anki, you'll notice that you're spending relatively long periods of time to create new cards, this is perfectly normal, it actually indicates that you're putting effort into writing useful cards, don't worry thought, it gets easier by time.

Everything I mentioned earlier applies to video content as well, the only difference is that instead of highlighting important parts, I type them, and sometimes I mark the important timestamps and go back to them after I'm done; I tend to use screenshots more often when creating cards for this type of content.

There is one last type of cards that I use, I call them "implementation cards", I don't have many of them, and they're all combined in the same deck; I use them for questions that require actual code as an answer, for example I have a card for implementing quick sort, and one that requires me to convert a JavaScript async function to use promises and a generator function instead; again, I use this type sparingly, because answering this type is time consuming.

There are many discussions regarding the "perfect" Anki deck configuration, for me, I use the default configuration with two minor changes, I increased the maximum number of new cards to 50 per day, and reduced the maximum review interval to 365 days.

A Philosopher, by Salvator Rosa

FAQ:

“But why memorize all of this? Just learn what you need as you go”

I learn a lot by simply googling problems that I face when doing my daily tasks, however, in my opinion, there are a few problems with this approach:

When learning something on the job, you’re usually trying to get something done, you don’t have the time to gain deep understanding of the problem or the solution; you probably won’t be able to see the bigger picture, or notice how the problem you're facing could be an indicator of a more critical problem; there is a good chance that you’re learning a single solution for a single problem, which isn’t necessarily bad, but you can certainly do better.
Leaning only what you need means that if you don’t face a certain problem, then there’s a good chance that you will learn little to nothing about it; if you’re a front-end developer, you're not going to face back-end related problems, does that mean that you should ignore everything back-end related? If you’re working with relational databases, does that mean that you shouldn’t read about noSQL databases? If you’re a fullstack JavaScript developer, does that mean that you shouldn’t explore other languages? Many people might argue that you shouldn’t, but I think you should.
Learning just enough is a passive way to level up, you should consider leveling up deliberately.

Also, if you have cards that cover fundamental concepts in your decks, then you should find technical interviews easier to do; you’re regularly reviewing your cards, so you won’t have to think about the phrasing of your answer during an interview; this also applies to implementation cards, they make preparing for white board interviews easier.

“Why not invest more time in learning by doing instead of doing all of this Anki stuff?”

learning by doing is great, however, there are a few things that you need to keep in mind:

when learning by doing, you might find that you're re-discovering patterns,what I mean by that is you might find yourself trying to describe a problem or a solution that already has a name, knowing the term that describes a specific problem or a solution makes communicating it more efficient; for example, in React, I didn’t know that passing the same prop multiple levels down is called “props drilling”; try googling your own description for props drilling, then google “props drilling”, notice how the results are better in the latter search.
always try to find similarities between technologies, even if they were completely different; for example, each operation in MongoDB's oplog is idempotent. That is, oplog operations produce the same results whenever applied to the target dataset, this is somewhat similar to how Redux works, if you call the same series of actions, you'll get the same resulting state, both of these behaviors are somewhat similar to the event sourcing pattern, they're not textbook implementations of it, but if you already understand one of them, you can use the same mental model to understand the other, and then you start to refine that mental model to accurately represent the new concept you're learning; what you're doing is that, instead of reasoning about a new concept as if it's completely new, you start to think of it as something close to a concept that you already understand well; it's important to note that you're not necessarily looking for "real" patterns, you're just looking for similarities that could help your understanding.

“What if I'm too busy to do my cards?”

consistency Is key here; even if you can’t do all the cards, then at least do some of them, the good thing is that even if you fail to answer some cards, you will simply see them more often, and you'll eventually have the answer memorized again.
Don’t feel bad if you have many late cards, the last thing you want is yet another thing that makes you feel bad about yourself; the fact that you’re reading this blog post is a proof that you’re genuinely trying to learn something, so don’t be too hard on yourself.

Lessons learned in modern UI testing

Ahmed Al-Obaidi — Fri, 10 Jan 2020 21:19:11 +0000

I've been developing modern React-based UIs for a few months now, while also maintaining not-so-modern ones, and I recently faced a problem: I've tested web services before, but on the front-end, I don't even know what to test; the problem wasn't that I couldn't find a tool to test with, there are many interesting testing libraries out there, the problem was that I didn't even know how to approach testing UIs to begin with; our front-end tech lead is nice enough to let us try things around, so I did, and it was .. well .. frustrating, I noticed that most of the tests that i was writing were either breaking easily or were downright useless, so I read articles here and there, and did Kent C. Dodds testing courses titled “JavaScript testing practices and principles” and “Testing React applications” that are available on Frontendmasters; below is a summary of what I think are the most important points that were mentioned:

Tests should not force you, or even encourage you, to rewrite parts of your implementation.
Code coverage is almost always a bad metric for how confident you are in the code you’re shipping; it’s also incorrectly used as a metric for code quality.
Code coverage tools implicitly assume that all blocks, statements, and lines of code are equal, but in reality, some are a lot more critical than others.
The last 10% of code coverage is usually covered by tests that are hard to maintain.
Tests should explicitly communicate the relationships between the expected result and other entities that are directly causing this result.
Tests that resemble how the entity is actually used give more confidence in that entity.
Always be explicit about your mocks.
When mocking, you must ensure that the mocked entity and the entity that you’re testing are actually connected as expected, for example if you're calling an API and you mock this call, then you must first ensure that the entity you’re testing is actually able to send requests to that endpoint, you don’t have to write a test to check this kind of connection, a manual check is enough.
In the formal definition of a unit test you mock every single external dependency, otherwise you're writing an integration test; when you mock everything you're focusing on this very specific entity that you're testing, it's fine to have shallow mocks as long as they behave as your entity expects them to behave.
Clean up your testing DB before each test instead of after, this ensures that if a test fails, your DB would be in a debug-able state.
testing the CSS, or the overall styling of an entity is usually best done using visual regression tools, but if you're doing CSS-in-JS then you can do snapshot testing that includes your CSS; this is considered a middle ground between regular tests and visual regression tests.
the problem with Enzyme is that it encourages testing implementation details, it causes extreme cases of white-box testing, for example: shallow rendering implicitly mocks all inner components even if they live within the same module/file, another example would be the “instance()” method, which gives you access to a component's class instance so that you can call methods directly, which encourages breaking the connection between the actual component and it’s methods.
Snapshots can include the props of your components; however, including them is considering an implementation detail, because users don’t care about props.
Good tests are the ones that would guide you through a refactoring process, tests that just fail when you do any kind of refactoring are not useful.
Do your best not to test state changes, users don’t care about how your internal state is changing, testing how these changes affect your UI is a lot more useful.
Snapshots can be easily abused; if someone runs a snapshot test, and it fails, and they don't carefully read the log before updating the snapshot, then this test is not even a test anymore; Snapshots heavily depend on the commitment of the team to be intentional about maintaining their tests.
Snapshots tend to have a higher signal-to-noise ratio, it's difficult for someone to tell which parts are important, and which aren't, that’s why we should keep our snapshots small.
Snapshots are useful not just for DOM and DOM-like assertions, but also for object equality assertions, and specific error throwing assertion; they are easier to maintain compared to manually writing down the equality check, which is the more common approach for those types of assertions.
If a component’s smoke test fails because it expects a provider ( Redux store, browserRouter, etc..) then you should simply render it with that provider.
It’s perfectly fine to first setup the test by doing manipulations that depend on implementation details in order to reflect a specific scenario that your test depends on, just make sure that the actual core of your test is not following the same approach.

I'm interested to see how things will go from here.
At the end I'd like to share this treasure with you.