Hacker News Reader

Comment by pjc50 | Hacker News Reader

I'm now wondering if I have enough material to do an interesting writeup for my time as a CPU bug-hunter in verification.

The client (a now vanished startup) had a small 8-bit CPU design which they wanted validation for, using the technique of executing random sequences of instructions and comparing the result against an emulator. We wrote the emulator independently from their architecture description. Given that most instructions were a single byte plus arguments and most of those were valid, the test coverage was pretty thorough. All looked fine until I added support for interrupts, at which point we discovered that an interrupt during a branch would not return to the correct point in execution.

Verifying security properties of processors is really hard; you can go looking for specific types of failure, but I'm not aware of a general way of proving no information leakage.

View on HN

I've done the same line of work in a larger-scale armv8 processor.

I think there is no answer that doesn't involve sign-offs on certain things.

In the situation you described, we resorted to fully randomizing everything, and then adding constraints to ensure it remained legal. This is a tedious process, one that leads to multiple false-positive failing tests.

However, the opposite situation, writing constrained stimulus from the beginning, leads to gaps where you didn't think of randomizing something, or you over-constrained it.

It's similar to a top-down vs down-up approach, only one is difficult and tedious and riddled with false positives, whereas the other one is easier and simpler, but can hide bugs.

In the face of issues like what you said, we implemented randomized interface behavior. Interrupts are always meant to be program-order invisible, so you can randomize those (imagine, 100 interrupts back to back, or 1 every N cycles where N is random but smaller than 5 or 500 etc). Pure random isn't interesting on its own. You need controlled randomness. From that point, you have to then start adding constraints for illegal/impossible situations, and you have to be extremely careful about these. We found a bug a week before tapeout when a senior architect forced a junior engineer(wonder who this is) to add a constraint. He used his seniority to sign it off, without going through a group review, and it was a mistake.

> but I'm not aware of a general way of proving no information leakage.

As I understand it, the current consensus is to use a tagged architecture, then show that there are no observable differences when the tags involve secret data and the value of the tagged data changes.

There are a few rubs here. One is that this is pretty hard to do. The other is that no one wants to pay the overhead of using a tagged architecture. Yet another is that deciding what "observable difference" means is challenging (too little, and you probably miss attacks, too much, and you will probably discover information leaks).

Further, this kind of rigorous system hasn't been rigorously empirically evaluated by a third party (as far as I know, perhaps in part because it's so hard to create these systems). "Empirically evaluated?" you scoff, "there's a proof, what's the point of testing?" Well...

For a glimpse of what this looks like, consider the SAFE architecture: http://www.crash-safe.org/assets/verified-ifc-long-draft-201... and lowRISC: http://www.lowrisc.org/downloads/lowRISC-memo-2014-001.pdf

Overhead of tagged architecture is to some extent an myth caused by abysmal performance of certain implementations (eg. iAPX whose performance problems are AFAIK caused mainly by funky instruction encoding) and by performance issues with "straightforward" way of running C code on such architectures.

I remember one of my professors in college talking about tracking down a register leak in the renaming block of an out of order processor he was working on. If you thought memory leaks could be annoying to deal with...

> but I'm not aware of a general way of proving no information leakage.

Cadence has a tool [1] to do this, but I'm not sure it would work for timing leaks.

[1] https://www.cadence.com/content/cadence-www/global/en_US/hom...

I've used this product and you can't jam the entire chip into it. You can only jam pieces of it before the search space is so big it runs forever. It is useful for smaller pieces, but it will eventually go critical and melt down your server farm if you keep growing the problem size. That was my experience a few years back.

There's actually been a lot of work in that going back five years or so. Here's a commercialized one:

http://www.ccs.neu.edu/home/pete/acl206/slides/hardin.pdf

Formal verification of specs, microcode, and security policy they hold in ACL2. Part of that is embedding a separation kernel a la MILS or SKPP model. It also has triplicated registers for fault-tolerance. Then, they integrate high-level languages like SPARK and microCryptol with that using certified compilers or equivalence checking.

Here's some examples from CompSci work:

https://eprint.iacr.org/2016/846.pdf

http://users.ece.utexas.edu/~tiwari/pubs/tiwari-dissertation...

http://cs.ucsb.edu/~sherwood/glift/

http://ieeexplore.ieee.org/document/7927266/

http://www.eecs.ucf.edu/~jinyier/papers/VTS12.pdf

http://www.cse.psu.edu/~dbz5017/pub/asplos17.pdf

Just also found a super-old one that tries to do it with capability-based mechanisms.

https://dl.acm.org/citation.cfm?id=803030

Most hardware work in information-flow analysis and control is currently focused on making hardware that controls bad software. I don't think most of them consider a CPU failure. If anything, they might be more vulnerable from a practical strategy of trying to reuse existing cores by making info-flow components that operate side-by-side with them. Here's an example from that area, though, since they could be modified to address recent concerns.

http://www.crash-safe.org/assets/verified-ifc-popl2014.pdf

http://csl.stanford.edu/~christos/publications/2010.hari_kan...

Reply on news.ycombinator.com