Random rants and pontifications by Gernot Heiser
There are multiple instances of authors comparing verification efforts of systems projects by looking at the ratio of proof to code size. I demonstrate why this is nonsense and constitutes a benchmarking crime.
Last month researchers reported that the data memory-dependent prefetcher (DMP) on Apple M1 chips can be used to break encryption. (And there are indications that similar attacks might be possible on Intel silicon.) The researchers observe that any (64-bit) aligned data word, whose value matches bits [53:32] of its own address, is considered a pointer [ ]
Machine learning is en vogue, being applied to many classes of problems. One of them is cybersecurity, where ML is used to find vulnerabilities in code, simulate attacks, and detect when an intruder has breached a system’s defenses. Ignoring that intrusion detection is an admission of defeat (it comes into play when your system is [ ]
In the final blog in this series I want to talk about how TS not only survived, but bounced back with a vengeance. This is much more fun to write than the previous blog, which was truly painful. I had to spend hours trawling through emails that made me re-live all the insanity, dishonesty, deceit [ ]
It s now almost 9 months since CSIRO s Data61 announced it was abandoning the Trustworthy Systems (TS) group. In previous blogs I have fact-checked the CSIRO CEO s Senate Estimates evidence as well as CSIRO s public statements about this, and pointed out how these statements omitted important facts or were outright dishonest. Before I leave this chapter [ ]
A few months back I fact-checked the CSIRO CEO s evidence to a Senate Estimates Committee hearing. At the time I promised more fact-checking of CSIRO’s communication about the abandoning of Trustworthy Systems (TS). Well, it has taken much longer than I hoped, mostly because I ve been working 60-hour weeks to undo the damage caused by [ ]
Following CSIRO s abandoning of Trustworthy Systems (TS) and the seL4 technology TS developed, the seL4 Foundation has seen a significant increase in Foundation membership, including a number of new Premium Members that get a seat on the Board. Among others, this has increased the Foundation s budget ten-fold – a great shot in the arm for [ ]
Great news: Ryan Barry from the Trustworthy Systems verification team has just completed the access-control proofs of seL4. What does this mean? In more detail: the proof shows that seL4 will only allow a thread to access an object or memory resource if the access is explicitly authorised by a capability. Specifically, user code cannot [ ]
On 3 June 2021, Dr Larry Marshall, CEO of CSIRO, gave evidence in an Estimates hearing in the Australian Senate. The official transcript is available from the Australian Parliament s web site. Senator Chisholm asked a number of questions regarding CSIRO s decision to abandon the Trustworthy Systems Group (TS), one of them Dr Marshall took on [ ]
CSIRO, Australia s national research agency, has just decided to disband the Trustworthy Systems (TS) team, the creators of seL4, the world s first operating system (OS) kernel proved correct and secure. TS is widely regarded and admired as the leader in the use of formal methods (mathematical proof techniques) to real-world software systems, and arguably the [ ]