This is neat but the analysis of their work leaves a bit to be desired. You can't just randomly select instructions and see if you did a good job, because the instruction space is not really uniform on any axis that people care about. For example, on a hypothetical ISA that has most the encoding space that is, like, simple arithmetic ops then you can get "good" coverage really easily. But that's not actually very useful because the instructions people care about when doing this kind of analysis are specific and usually more esoteric, and difficult to analyze with a simple bitstring approximation. Like, this definitely cannot discover the semantics of syscall, or rdrand. The authors claim they would have been able to discover reptar if they extended their work slightly, but I think it is pretty dubious that their methodology is powerful enough to do so.
Reminds me of sandsifter, a fuzzer for the x86 ISA:<p><a href="https://github.com/xoreaxeaxeax/sandsifter">https://github.com/xoreaxeaxeax/sandsifter</a>
This is interesting work but it totally misses the boat when it talks about the current state of the art. They cite a 2014 version of the Goel-Hunt-et al formal x86 model in ACL2, but they fail to talk about its modern version. The modern version (developed at Centaur and then Intel!) is an ACL2 x86 model that is so precise that it can boot Linux and run user-land programs. Let me say that again: it is a formal mathematical model of a processor that is so precise that it can boot Linux and run user-land programs! This is a monumental accomplishment and is not even mentioned in their paper.
I've long wanted to have a way to see what actually happens inside a CPU when a set of instructions are executed. I'm pretty excited after skimming this paper as it looks like they developed a technique to automatically determine how the x86-64 instructions actually work by observing real world CPU behavior.