[HN Gopher] Basic SAT model of x86 instructions using Z3, autoge...
___________________________________________________________________
Basic SAT model of x86 instructions using Z3, autogenerated from
Intel docs
Author : djoldman
Score : 131 points
Date : 2023-05-15 10:35 UTC (12 hours ago)
(HTM) web link (github.com)
(TXT) w3m dump (github.com)
| mdaniel wrote:
| This is unlicensed, as best I can tell, as is the parsing
| submodule (https://github.com/zwegner/sprdpl)
| bjourne wrote:
| What is the engine satisfying?
| fooker wrote:
| It is common to express denotational semantics as SAT/SMT
| expressions.
|
| For example, consider a function f(x) = x << 1.
|
| A valid sat semantics for this function is: y == f(x) implies y
| == 2 * x.
| bjourne wrote:
| But what variable assignment is being SATisfied?
| fooker wrote:
| if f(x) == g(x) is satisfiable, you get one value of x for
| which f(x) == g(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.
| mattst88 wrote:
| This is very interesting. I'm going to be excited to see what
| neat things can be done with it.
| userbinator wrote:
| _find a bug in Intel 's pseudocode_
|
| It'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/
| chc4 wrote:
| 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.
| rep_lodsb wrote:
| 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?
| chc4 wrote:
| 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.
|
| 0: https://xenproject.org/2012/06/13/the-intel-sysret-
| privilege...
| hedora wrote:
| The X86-TSO paper is great if you want to learn how to write
| code for intel machines with more than one core:
|
| 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...
| gnufx wrote:
| I don't remember what they cover, but Sewell's group also
| have models for ARM and POWER which must be referenced from
| https://www.cl.cam.ac.uk/~pes20/
|
| 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...
| jcranmer wrote:
| If you want to be pedantic, this isn't from the official
| documentation (that's the bajillion-paged manual of every
| instruction), it's from the intrinsics guide here:
| https://www.intel.com/content/www/us/en/docs/intrinsics-guid...
|
| 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.
| CamperBob2 wrote:
| 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?
| insulanus wrote:
| This type of thing can help you formally verify code.
|
| 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/
| peterfirefly wrote:
| It's all about model checking:
|
| 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.
| weinzierl wrote:
| Could this be used to show that two programs (with only
| instructions from the covered subset) are equivalent?
| boomanaiden154 wrote:
| 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].
|
| 1. https://github.com/AliveToolkit/alive2
|
| 2. https://sel4.systems/
| aqrit wrote:
| This was for a super optimizer.
___________________________________________________________________
(page generated 2023-05-15 23:01 UTC)