ToySMT – simple SMT solver under ~1500 SLOC of pure C.
It’s very early sneak preview. It supports only bools and bitvecs. No integers, let alone reals and arrays and tuples and whatever. However, it can serve as education tool (hopefully). It parses input SMT-LIB file (see “tests” and “examples”), constructs digital circuit, which is then converted to CNF form using Tseitin transformations. This is also called “bitblasting”. minisat is then executed, as an external SAT solver. Stay tuned, it will be evolved. Aside from SMT-LIB standard, I also added two more commands: (get-all-models) and (count-models) (see “tests”). Since it’s early preview, it was only checked on “tests” and “examples” you can find here. Anything else can fail. Also, error reporting is somewhat user-unfriendly. First, you can check your .smt files using other SMT solver (I used z3, Boolector, STP, Yices, CVC4).[…]
Diagram highlights some major tools and ideas of pure symbolic execution, dynamic symbolic execution (concolic) as well as related ideas of model checking, SAT/SMT solving, black-box fuzzing, taint data tracking, and other dynamic analysis techniques.
Covert Shotgun: Automatically finding SMT covert channels:
In my last blog post I found two covert channels in my Broadwell CPU. This blog post will again be about covert channels. For those unfamiliar a covert channel is a side channel where the attacker has an implant in the victim context and uses his channel to “smuggle information” in and out of the victim context across existing security boundaries. In this blog post I’ll explore how we can automate finding SMT covert channels. SMT is intel speak for hyper threading. Before I proceed I should note that one of the two covert channels I found in my last blog passed, the one based on the RdSeed instruction, appears also to have been found by others. You can read about it in D. Evtyushkin & D. Ponomarev . They will be presenting their work on this channel at CCS. Unlike myself they develop the channel fully and discuss mitigations. So if you find this channel interesting their paper is well worth a read. […]