Intel has had a couple of major events that totally changed their attitude to verification. The first was in 1994 when they had the Pentium floating-point divide bug and management said “don’t ever let this happen again”. In 1996, they started proving properties of the Pentium processor FPU. (For more details, you can read my 2012 post on Semiwiki.)

Then, a couple of years ago, the side-channel vulnerabilities like Spectre were discovered. These didn't just affect Intel, it turned out every modern CPU had the same problem hiding in plain view for 20 years. Basically, the vulnerability plays on speculative execution making memory references and then being able to discover which memory elements were accessed, even though the speculative execution got abandoned. (I've written a lot about this so if you don't know what all this means, is then start at Spectre/Meltdown & What It Means for Future Design.)

At the recent Jasper User Group, Eli Singerman of Intel gave one of the keynotes about how they were using formal to verify processor security. As a starting point, let me emphasize that attacks like Specre are not due to incorrect implementation. So the most powerful formal tool in the world would declare all these processors good. They meet their specs. The problem is that their specs say what the processor should do but omit what it should not. It turns out that loading something into a cache and not using it (and some other stuff) is things processors should not do.

This is new at Intel. As Eli said:

We've just started in this, so there are lots of challenges and opportunities. Next year we’ll have much more experience and I hope we can talk to that.

Eli pointed out that Amir Pnueli in the 1996 Turing Award lecture pointed out that formal verification engineer was a future profession. Today there are over 9,000 formal verification engineers using Cadence's JasperGold platform, so that day has arrived.

Platform Security

Platform security is very important. Security defects are both very visible and very expensive. Each layer needs to be handled, as well as the cross-layer flows. So that means SoC (and IP) hardware at the lowest level, then up to BIOS (or UEFI these days), the operating system such as WindowsX or Linux, and then the applications. There might be a hypervisor in there somewhere, too.

Eli said that there is a feeling that firmware is less critical since they don't require a silicon respin. That was perhaps true a few years ago. But firmware bugs hide hardware bugs, and, from a security perspective, mitigations for attacks are often in firmware. So firmware verification is very important.

Each layer validates the layer about in security (hardware root of trust, etc).  Intel doesn't control the higher levels, but they want to ensure the lower levels are secure. It is a kind of contract.

The side-channel attacks like Spectre were a huge problem. Intel has been fixing processors that have been in the field for seven years. These fixes affect performance negatively and cost a lot of money. There are new attacks showing up on a regular basis. 

He said:

We are trying with this formal approach to get more into prevention and somehow guarantee we won’t get these kinds of things in the future. We're moving from defensive to proactive. As we speak, the problem is growing.

The problem is growing since there are maybe 30-40 IP-blocks at Intel that are running firmware on embedded controllers. Security firmware itself is not the biggest problem, it is all the other firmware. At Intel, firmware used to just mean microcode on the processors themselves, that was coded up at Intel in an (Eli's word) obscure language. But now there is IP buried in the hardware and it is running software. The software is pre-defined, a fixed program, so we call it firmware. (By the way, back in the 1980s I came up with the term stiffware. This is software that works but where the source code has been lost, or the compiler, so it can never be altered. I came up with the term when I went on sabbatical and there was a screwup with backups, and we lost the source code to a program I was responsible for. It became stiffware.)

So today firmware is all over at different levels. The lowest level is core firmware or microcode. This implements the higher-level machine-code instructions. An Intel processor behaves as a RISC processor even though it has a a CISC instruction set. The translation is handled by microcode. Then there is BIOS platform initialization.

Part 2

I will cover the second half of his important presentation tomorrow.

Sign up for Sunday Brunch, the weekly Breakfast Bytes email.