The postmortem is a major technique to learn failure in Site Reliability Engineering (SRE). SRE people also submits that such failure may be avoided by resolutions. Same approach is found at industrial companies. It's root cause analysis.
On the other hand, are these postmortems common in open source culture? No, unfortunately.
This project's goal is finding resolutions, such as language or verifier, which are suitable to avoid failures or bugs, which causes security incident.
We are focusing on FreeBSD kernel today, because it has many informations about the bugs on their security advisory.
There are two choices. First is re-writing a part of operating system with language or verifier. The part should re-write the patch of security incident and be runnalbe. But this approach needs huge human resource.
Second is writing small pseud code to be proved or verified. Now, we are choosing this approach with small resource.
Our pseud code is found at following:
An example of ATS2 language
For example, the ATS2 pseud code causes compile error,
because the code forgets fdrop after calling copyin.
This mistake occurred at FreeBSD-SA-19:15.mqueuefs.
It means this bug may be avoided, if FreeBSD was written by ATS2 language.
You can add fdrop calling to fix this bug.
An example of VeriFast verifier
For example, the C pseud code with annotations causes error on verification,
because the code just returns without calling fdrop.
This mistake occurred at FreeBSD-SA-19:15.mqueuefs.
It means this bug may be avoided, if FreeBSD was verified by VeriFast verifier.
You can write goto out instead of return error to fix this bug.
- ATS-Postiats to prove ATS2 code
- GCC to compile C code translated by ATS2
- VeriFast to verify C code with annotations
We are testing this program on Debian GNU/Linux.
$ git clone [email protected]:metasepi/postmortem.git
$ cd postmortem
$ make
- Advisers kindly support this project