This led to some fun times, like the infamous POP SS bug (CVE-2018-8897), which was a privilege escalation vulnerability in basically every kernel on Intel CPUs. But it didn't affect AMD CPUs, because they implemented the instruction as written in the x86 specification, which didn't have the bug that hardware did.
That behaviour is actually documented though? It seems to be a corner case that OS developers didn't pay attention to until it was exploited.
It goes all the way back to 1980, where a revision to the 8086 introduced this to prevent an exception or non-maskable interrupt from using an incorrect stack pointer (by making MOV SS / POP SS atomic with the next instruction, which must load SP).
Arguably it should no longer be necessary in ring 3 protected mode, since the stack will be switched automatically - unless the handler itself was in ring 3, but no current OS allows that?
Woops, sorry, I was actually thinking of the SYSRET vulnerability (CVE-2012-0217) which was a mismatch between Intel and the written spec[0]. POPSS did also have differences between Intel and AMD implementations but both were vulnerable in different ways.
It is relevant here because none of the documentation the authors found was correct, so they wrote this and confirmed it matched observed hardware behavior.
Ideally, it should pull from the same master repository of information, but given my limited experience with how documentation tends to get built, I would be not at all surprised to learn that it's copy-pasted between several different projects, so that bugs in one don't get reflected in others.
Count me in. Any kind of formalization is empowering, but what practical applications can it have? I'm sure there are quite few of them, but what are they?
As an extremely experienced dev with a ton of Intel assembly experience, I'll confess I have no earthly idea what this is, what it does, who needs it, or what inspired it. Any good pointers to tutorials or introductory material?
This guy's code produces Z3 theorems for a subset of the x86 instructions. By theorems, I mean "mathematical statements about how they work".
They can be combined so that a small(ish?) piece of x86 code can be turned into a model, which Z3 can prove (or disprove) statements about.
This is very useful for proving a piece of code right or wrong.
Model checking used to require a phd -- now it just requires a bit of effort and "mathematical maturity". We have come a long way towards making it a generally available tool for all/most programmers but there is still a long way to go.
You can use it to (mostly) validate small snippets are the same. See Alive2 for the application of Z3/formalization of programs as SMT for that [1]. As far as I'm aware there are some problems scaling up to arbitrarily sized programs due to a lack of formalization in higher level languages in addition to computational constraints. With a lot of time and effort it can be done though [2].
24 comments
[ 3.3 ms ] story [ 62.2 ms ] threadIt's well-known that the official docs have bugs; others have had success using AMD's to compare:
https://www.os2museum.com/wp/sgdtsidt-fiction-and-reality/
It goes all the way back to 1980, where a revision to the 8086 introduced this to prevent an exception or non-maskable interrupt from using an incorrect stack pointer (by making MOV SS / POP SS atomic with the next instruction, which must load SP).
Arguably it should no longer be necessary in ring 3 protected mode, since the stack will be switched automatically - unless the handler itself was in ring 3, but no current OS allows that?
0: https://xenproject.org/2012/06/13/the-intel-sysret-privilege...
https://pages.cs.wisc.edu/~markhill/restricted/cacm10_x86-TS...
It is relevant here because none of the documentation the authors found was correct, so they wrote this and confirmed it matched observed hardware behavior.
Now, I just need to find the equivalent for arm…
For anyone who hasn't encountered one, Sewell gives excellent talks, e.g. at CCC, most recently https://media.ccc.de/v/35c3-9647-taming_the_chaos_can_we_bui...
Ideally, it should pull from the same master repository of information, but given my limited experience with how documentation tends to get built, I would be not at all surprised to learn that it's copy-pasted between several different projects, so that bugs in one don't get reflected in others.
For example, consider a function f(x) = x << 1.
A valid sat semantics for this function is: y == f(x) implies y == 2 * x.
if f(x) != g(x) is satisfiable, you get one value of x for which f(x) != g(x)
Both of these are useful in practice.
x is the set of inputs to an instruction.
So, if your proof is correct, and your description of the (language/CPU) is correct, you can prove the code does what you think it does.
Formal proof systems are still growing up, though, and they are still pretty hard to use. See Coq for an introduction: https://coq.inria.fr/
https://en.wikipedia.org/wiki/Model_checking
Three of the pioneers of model checking won the Turing Award back in the noughties:
https://amturing.acm.org/award_winners/clarke_1167964.cfm
https://amturing.acm.org/award_winners/emerson_1671460.cfm
https://amturing.acm.org/award_winners/sifakis_1701095.cfm
Z3 is an amazing theorem prover, bordering on magic.
https://en.wikipedia.org/wiki/Z3_Theorem_Prover
Theorem proving is often used in model checking.
This guy's code produces Z3 theorems for a subset of the x86 instructions. By theorems, I mean "mathematical statements about how they work".
They can be combined so that a small(ish?) piece of x86 code can be turned into a model, which Z3 can prove (or disprove) statements about.
This is very useful for proving a piece of code right or wrong.
Model checking used to require a phd -- now it just requires a bit of effort and "mathematical maturity". We have come a long way towards making it a generally available tool for all/most programmers but there is still a long way to go.
1. https://github.com/AliveToolkit/alive2
2. https://sel4.systems/