“And e’er the twain shall meet.”
“I need to talk to you about the kernel’s debug API code,” Dr. Rafal Kolanski said, approaching me with a sense of urgency. “We have a deadline and we won’t have the time to verify the debug-API for ARM – and we’ll barely be able to deliver the ARM-hyp proofs on time even if we skip it.”
“How can I help?” I asked Rafal lazily.
“Can you hide the debug-register context switching code in the verified build of the kernel?” Rafal asked, brows furrowed ever so slightly.
I sat up and paid attention. Our proof engineers often request small (or large) posthumous tweaks of the seL4 kernel codebase in order to make it verifiable. These tweaks may often introduce eccentricities into the code – but they each have a reason behind them. My investigation was about to begin. I found a way to hide this feature without compromising the feature’s functionality – and so the kernel was tweaked; another milestone in the successful collaboration between the kernel and verification teams.
I want to invite our readers to see how we co-ordinate things internally – let me unveil to you the fabric that entwines our Kernel and Verification engineering teams together.
It occurred to me that we could try to open a window of view into how the Kernel team and the Verification team here at Trustworthy systems really interact and in what ways we interact; it’s a push and pull cycle: we write code and verification takes a look through it; after digesting carefully, they come back and tell us what modifications would make it easier for them to reason about the code. Usually that’s the end of it, unless the particlar changes requested by the Verification team would introduce unacceptable performance overheads. Very seldom does the kernel team push back against verification.
We don’t yet have a SDLC (Software Development LifeCycle: a formal approach to software development) so to speak; we’ve just roughly developed an in-house rhythm between the two teams. Generally, it starts like this: verification sees some code we wrote, and they puzzle over it for a few hours. Then they send a diplomatic mission to query the kernel team about the code they are puzzling over. That analogy is surprisingly apt in practice because it usually looks similar to a delegation of dignitaries crossing the floor.
After a round of verbose inquiry, the verification mission will return to their mothership (Usually Gerwin’s office). A short while later, they will have brainstormed a series of “invariants” to begin with. These invariants are a set of properties about the kernel that are maintained across kernel invocations that are required for correct execution. These invariants are proven through the use of Hoare logic, in the form of preconditions which are true before any step of execution and postconditions which are true after the step.
They will then launch a second diplomatic mission. During this round of talks, they will explain the invariants they have come up with, and ask us if those invariants actually describe the code we’ve written.
Finally, depending on how complex the code being verified is, over the next few days, we will negotiate over our shared understanding of the code, and then take pointers from verification on ways in which we can make the code more amenable to the application of formal methods. This process may be repeated over the course of a few weeks depending on how complex the code in question is.
The end result? A mutual understanding, and later, a proof.
I asked Rafal to tell me, as a senior proof engineer, what he thought the useful outcomes from the teams’ discussions were. These were his insights:
As a final comment, making the meaning of the code explicit tends to gradually refine the code itself by making the kernel team look through the code not just from a top down or bottom up functionality perspective, but also as an overall composite system.
Drs. Gerwin Klein and June Andronick, our champion verification minds, have an interest in structuring our interactions into some form of SDLC – a formal discipline that can be replicated by other companies scalably to encourage the adoption of formal methods.
Would the discipline that arises from this aspiration be of a “Waterfall” nature? Or an “iterative” nature? Given the fact that verification needs multiple iterations of negotiation with the kernel engineers, a highly responsive, interactive and iterative process seems to recommend itself.
Yes: we have strong reason to believe so. As a result of the gradually increased mutual understanding between the two teams we have established a sort of rapport which has gone a long way to reducing the time that it takes to develop proofs. I turned to Joel Beeren, one of our lead Proof Engineers to get a feel for what factors have enhanced our proof engineers’ productivity:
A lot of the story between our teams has been about learning the expectations that we have of each other and what things make our respective jobs easier.
For the kernel development team, writing code that is amenable to verification takes a slight understanding of what things the verification team is likely to be uncomfortable with. For the verification team, they have to keep in mind that even if an amendment would make it easier to reason about and verify the code, all such amendments must not compromise the performance of the kernel unreasonably.
I asked Joel Beeren, one of our more experienced Proof Engineers whether, in his experience, the strides we’ve made are more as a result of the verification team coming to understand the kernel team’s needs better or whether they’ve come about more as a result of the kernel team coming to understand the verification team’s requirements better.
He feels that the understanding that both of our teams each have of the other is essentially of equal weight. I guess it’s like push and pull.
Formal methods are the future of high-assurance systems. You can consider this your invitation to see how we accomplish our verification goals, and maybe you can leave a comment or two: do you have any insights on what kind of SDLC could arise that integrates traditional software development and formal methods?
We like answering the tough questions. Come challenge us on our mailing list. Keep an eye out for more posts in this series, In Lockstep, on this blog, and check out some of our other posts too. Drop us a line on our IRC Channel. G’day!