PACMAN and Using Jasper for Security Verification

At the recent Jasper User Group meeting, there were a couple of presentations on using the Jasper apps for security verification, specifically Jasper SPV (for Security Path Verification):

• HW Security Path Validation Using Formal Methods: Intel Case Studies by Alex Levin of Intel (winner of the best presentation award)
• Towards Enabling Security Formal Verification of the Load-Store Unit of A-class Arm CPUs using SPV App by Madhu Iyer of Arm

These papers were too detailed (lots of scripts and options) for a general Breakfast Bytes post, so I'll try and give you an idea of the flavor of the approaches.

If I had to sum up the strengths and weaknesses of formal verification, I would say that it is great at finding corner cases that nobody had ever thought of. On the other hand, just proving that the normal case works (say that Ethernet packets are correctly received) can be cumbersome. Attempting cyberattacks on a device have something in common: the normal case is not going to be a security vulnerability, so you will need to look to some obscure corner to find a vulnerability.

Security Vulnerabilities

The three big security vulnerabilities of processors in the last few years were:

• Meltdown
• Spectre
• PACMAN

I have written about Spectre and Meltdown before, starting with my post the day that the existence of the vulnerabilities was discovered, and then in more follow-up posts:

• What Is Meltdown? How Can It Affect Both Intel and Arm?
• Spectre and Meltdown: An Update
• After Meltdown and Spectre

I will explain Meltdown, since it is the simplest. It was also the easiest to fix, but it remains a good choice for proving security because it is simple. Data is extracted under the cover of an exception.

Meltdown consists of the steps:

1. Prepare the cache by ensuring that you have a page of cache where none of the lines are in the cache (cold)
2. Access a byte of memory that you should not and load it into a register
3. Use that register to make an indirect reference into the cache
4. Inspect the cache and see which line is now in the cache (warm) and that gives you the value of the forbidden byte

The reason this worked is that, on (some) Intel processors, the legality check for the access was done in parallel with the access. So the register was loaded just before the processor noticed that the access was illegal and faulted. In the long term, the solution was not to do that. In the short term, the solution was to move system memory out of every process' address space.

PACMAN

The most recent vulnerability is PACMAN. You know it is a serious vulnerability since, like Spectre and Meltdown, it has its own logo.

You can read the original paper PACMAN: Attacking ARM Pointer Authentication with Speculative Execution. This paper uses as an example the Apple M1 chips, since it is easy to put a Macbook in another room and access it over Ethernet, demonstrating that no access to the hardware was required. But on the Arm page, PACMAN security vulnerability Arm lists the affected processors, which includes many of the high-end Arm processors, such as the Neoverse N2, Neoverse V1, Cortex A710, and more. The thing that is common to the affected processors is that they use pointer authentication codes (PACs).

So what is a PAC? A 64-bit processor doesn't use the high-order bits of the address since you can't use that much memory (16 exabytes). To increase security, addresses (pointers) use the high-order bits as a sort of capability. See my recent post HOT CHIPS: Arm's Morello for more on that). Quoting from Arm's page:

Pointer Authentication protects pointers in memory from malicious tampering by prepending a cryptographic code (or PAC) into the unused upper bits of the address. This code acts as a signature, and it is validated before the dereference of the pointer (on an indirect branch or memory access). If the pointer has been tampered, then the authentication will very likely fail, and the CPU will fault, thereby thwarting the attack.

The reason that it says "will likely fail" is that if you put a random number in those high-order bits, you might get lucky. PACMAN creates what they call an "oracle" to find out which are the correct bits by having a way to try them all. To do this, it is necessary to find a way to try a pointer and see if it passes or fails authentication. Whether or not it does can be detected in microarchitectural side effects. Shown graphically, from the Arm page:

The thing that caused a stir when the PACMAN paper was first published is that it is a hardware bug and so cannot be patched in the field. It is not considered that serious since it requires other security failures to cause anything bad to happen. Plus, before PACs were added, all processors were vulnerable to this attack since there was no PAC-based security to get around. Or, as Arm says:

Users should be aware that software that is not built using Pointer Authentication is already vulnerable to ROP/JOP style attacks, and so PACMAN is not needed to perform those attacks on that software.

Taint

The basic way to use formal techniques for this sort of vulnerability is to mark the data you are worried about with what is called a taint. By marking the data with this unique tag, it is possible to prove that there is no path from A to B, that the taint can never appear at B.

So, for example, in the Meltdown case, A might be the secret byte and B might be the register file (or a particular register to keep the proof simpler). If the tainted secret byte can get into a register, then there is a security vulnerability. 

The weakness of this approach is that you cannot just throw Jasper SPV at a design and have it discover this type of vulnerability. They rely on subtle interactions in the microarchitecture and extracting data through side channels. You can focus Jasper SPV on the specific vulnerability and use it to prove that the vulnerability exists. Then, when you have fixed it, you can use Jasper SPV to prove that the fix is good.

The dream is not to prove that you have fixed these three known attacks, useful as that is, but rather to identify the next such vulnerability before the bad guys do. Perhaps the most extraordinary thing about Spectre and Meltdown is that they were hiding in plain sight for twenty years before someone published papers about them. But a general rule in security is that if you discover a vulnerability that can be used without detection, then bad guys are already using it.

Learn More

See the Jasper SPV product page.

Tomorrow

Tomorrow is a Cadence global recharge day. Breakfast Bytes will not appear.

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