Recently a zero-day exploit (CVE-2021-31440) was found in the Linux kernel eBPF module. We will show how this bug could have been discovered and prevented using formal verification. A relatively simple logical error caused this bug, but it is easy to overlook and could lead to grave security implications. The bugs like this are difficult to find via exhaustive testing as the space of value combinations you need to test to stumble on it is relatively big. The typical way to find these bugs is by expert code reviews. Formal verification is offering another way to prevent or find bugs like this. Instead of spending the expert’s time pouring over the code looking for potential bugs, the specification is created, formally stating what the code is supposed to do. Then, using a proof assistant, a proof is developed that the given implementation satisfies this specification. If this proof is successful, it provides a bullet-proof guarantee that the code is correct wrt spec. Sometimes, as we will see in this example, the correctness could not be proved, which indicates that the implementation contains a bug. In this example, we will:
- Write a formal specification.
- Try to prove correctness for the buggy version of the code.
- Prove the correctness of the patched version of the code.
(Image: © Josh Edelson / AFP) 
With the number of COVID-19 cases rising, government officials around the world are taking various measures to stop the virus spread by canceling events, issuing warnings against public gatherings and closing offices. Many organizations are faced with the reality of remote work and not all of them are ready. 
Last month, we’ve attended HIMSS19. If you are not familiar with the event, Healthcare information and Management Systems Society (HIMSS) is an annual healthcare information conference, which brings together more than 45,000 healthcare and information technology professionals from all over the world. 
