Specifically, it had no way to "extend" its consistency model out to consumers of its messages, and so if consumers were also producers, then this distributed system as a whole could enter into a state where parts of it are lying to itself!

Otherwise, there were some really fun things you could do with it. For example, we could have per-client databases that would bring themselves up-to-date given the differential outputs of the server database. This would let you engage in a kind of manual sharding of data.

[1] https://www.petergoodman.me/docs/dr-lojekyll.pdf

Our understanding of ClangIR is that it has side-stepped the problem of trying to relate/map high-level values/types to low-level values/types -- a process which the Clang codegen brings about when generating LLVM IR. We care about explicitly representing this mapping so that there is data flow from a low-level (e.g. LLVM) representation all the way back up to a high-level. There's a lot of value and implied semantics in high-level representations that is lost to Clang's codegen, and thus to the Clang IR codegen. The distinction between `time_t` and `int` is an example of this. We would like to be able to see an `i32` in LLVM and follow it back to a `time_t` in our high-level dialect. This is not a problem that ClangIR sets out to solve. Thus, ClangIR is too low level to achieve some of our goals, but it is also at the right level to achieve some of our other goals.

P.S. your logo is surprisingly similar to that of ForAllSecure [3], which also provides a symbolic execution engine called Mayhem [4].

[1] https://klee.github.io/ (online example: http://klee.doc.ic.ac.uk/)

[2] https://github.com/trailofbits/deepstate#readme

[3] https://forallsecure.com/

[4] https://users.ece.cmu.edu/~aavgerin/papers/mayhem-oakland-12...

[1] https://github.com/trailofbits/deepstate

[1] https://github.com/trailofbits/mishegos

[2] https://blog.trailofbits.com/2019/10/31/destroying-x86_64-in...

[1] https://smallcultfollowing.com/babysteps/blog/2018/04/27/an-...

[1] https://github.com/vmware/differential-datalog

Souufle has been used in Ddisasm [5] for disassembling binaries. XSB Prolog has been used in OOAnalyzer [6] for inferring class hierarchies and virtual tables in binaries as well.

I myself spend some time working on datalog compilation for program analysis and decompilation :-)

[1] https://semmle.com

[2] https://souffle-lang.github.io/index.html

[3] https://bitbucket.org/yanniss/doop/src/master

[4] https://suif.stanford.edu/bddbddb

[5] https://github.com/GrammaTech/ddisasm

[6] https://resources.sei.cmu.edu/library/asset-view.cfm?assetid...

Another alternative, which I believe are both options available with PIN and DynamoRIO, is to implement or use an existing ELF loader, forking yourself, and loading in the target binary of interest at a known location.

One cool example of expression indexes is this: you want to store structured data (e.g. a protobuf) 'natively' in an SQL database, but still give the database visibility into the data stored in that serialized protobuf. You can create an expression index with functions that can read into the protodbuf data and give SQLite that visibility. Another benefit of things like expression indexes is storing comrpessed data. E.g. you want to store a big blob of compressed data, and give SQLite some access to it, but not access to all of it.

In the near future, we'll be transitioning another open-source Trail of Bits project, McSema [1], to using this wrapper. McSema currently stores lots of data in protocol buffers, which isn't very convenient for some reasons. Transitioning over to an SQLite database, hidden behind an API, is going to make things a lot nicer.

[1] https://github.com/trailofbits/mcsema

Glad that DeepState had an impact on you :-D We continue to evolve DeepState, both in the direction of better fuzzing, and better test case reduction.

Remill is instruction granularity, and so all it requires is raw bytes. McSema uses Remill in conjunction with a disassembly frontend (IDA Pro, Binary Ninja, or Dyninst).

If you have source code you can likely be more precise/efficient. Sometimes you may have access to source but not the ability to change/influence the build.

I think there's a lot of room for improvement with KLEE. If I were to write an LLVM symbolic executor from scratch then I think I would do some things differently.