# Fault Analysis on RSA Signing

This spring and summer, as an intern at Trail of Bits, I researched modeling fault attacks on RSA signatures. I looked at an optimization of RSA signing that uses the Chinese Remainder Theorem (CRT) and induced calculation faults that reveal private keys. I analyzed fault attacks at a low level rather than in a mathematical context. After analyzing both a toy program and the mbed TLS implementation of RSA, I identified bits in memory that leak private keys when flipped.

## The Signature Process with RSA-CRT

Normally, an RSA signing operation would use this algorithm: s=md (mod n). Here, s represents the signature, m the message, d the private exponent, and n the public key. This algorithm is effective, but when the numbers involved increase to the necessary size for security, the computation begins to take an extremely long time. For this reason, many cryptography libraries use the Chinese Remainder Theorem (CRT) to speed up decryption and signing. The CRT splits up the single large calculation into two smaller ones before stitching their results together.

Given the private exponent d, we calculate two values, dp and dq, as: dp=d (mod (p-1)) and dq=d (mod (q-1)).

We then compute two partial signatures, each using one of these two numbers; the first partial signature, s1, equals mdp (mod p), while the second, s2, equals mdq (mod q). The inverses of p (mod q) and q (mod p) are calculated, and finally, the two partial signatures are combined to form the final signature, s, with s=(s1*q*qInv)+(s2*p*pInv) (mod n).

## The Fault Attack

The problem arises when one of the two partial signatures (let’s assume it’s s2, calculated using q) is incorrect. It happens.

Combining the two partial signatures will give us a faulty final signature. If the signature were correct, we would be able to verify it by comparing the original message to se (mod n), where e is the public exponent. However, with the faulted signature, se (mod p) will still equal m, but se (mod q) will not.

From here, we can say that p, but not q, is a factor of se-m. Because p is also a factor of n itself, the attacker can take the greatest common denominator of n and se-m to extract p. n divided by p is simply q, and the attacker now has both of the private keys.

## Faulting a Toy Program

I began by writing a simple toy program in C to conduct RSA signing using the Chinese Remainder Theorem. This program included no padding and no checks, using textbook RSA to sign fairly small numbers. I used a debugger to modify one of the partial signatures manually and produce a faulted final signature. I wrote a program in Python to use this faulted signature to calculate the private keys and successfully decrypt another encrypted message. I tried altering data at various different stages of the signing process to see whether I could still extract the private keys. When I felt comfortable carrying out these fault attacks by hand, I began to automate the process.

### Flipping Bits with Manticore

I used Binary Ninja to view the disassembly of my program and identify the memory locations of the data that I was interested in. When I tried to solve for the private keys, I would know where to look. Then, I installed and learned how to use Manticore, the binary analysis tool developed by Trail of Bits with which I was going to conduct the fault attacks.

I wrote a Manticore script that would iterate through each consecutive byte of memory, alter an instruction by flipping a bit in that byte, and execute the RSA signing program. For each execution that did not result in a crash or a timeout, I used the output to try to extract the private keys. I checked them against the correct keys by attempting to successfully decrypt another message. With all of this data, I generated a CSV file of the intermediate and final results from each bit flip, including the partial signatures, the private keys, and whether the private keys were accurate.

Fig. 1: Excerpt from code to find faultable addresses in toy program

### Results

I tested a total of 938 bit flips, and I found that 45 of them, or 4.8%, successfully produced the correct private keys. Nearly 55% resulted in either a crash or a timeout, meaning that the program failed to create a signature. Approximately 31% did not alter the partial signatures.

Fig. 2: Output of analysis code

Fig. 3. Bit flip results for toy program

This kind of automation offers a massive speedup in developing exploits for vulnerabilities like this, as once you simply describe the vulnerability to Manticore, you get back a comprehensive list of ways to exploit it. This is particularly useful if you’re able to introduce some imprecise fault (e.g. using Rowhammer) as you can find clusters of bits which, when flipped, leak a private key.

## Faulting mbed TLS

Once I had the file of bit flip results for my toy program, I looked for a real cryptographic library to attack. I settled on mbed TLS, an implementation that is primarily used on embedded systems. Because it was much more complex than the program I had written, I spent some time looking at the mbed TLS source code to try to understand the RSA signing process before compiling it and looking at the disassembled binary using Binary Ninja.

One key difference between mbed TLS and my toy program was that signatures using mbed TLS were padded. The fault attacks I was trying to model are applicable only to deterministic padding, in which a given message will always result in the same padded value, and not to probabilistic schemes. Although mbed TLS can implement a variety of different padding schemes, I looked at RSA signing using PKCS#1 v1.5, a deterministic alternative to the more complex, randomized PSS padding scheme. Again, I used a debugger to locate the target data. When I knew what memory locations I would be reading from, I began to fault one of the partial signatures and produce an incorrect signature.

I soon realized, however, that there were some runtime checks in place to prevent a fault attack of the type I was trying to conduct. In particular, two of the checks, if failed, would stop execution and output an error message without creating the signature. I used the debugger to skip over the checks and produce the faulted signature I was looking for.

With the faulted signature and all of the public key data, I was able to replicate the process I had used on my toy program to extract the private keys successfully.

### Automating the Attacks

Just as I had with the toy program, I started to try to automate the fault attacks and identify the bit flips that would leak the private keys. In order to speed up the process, I wrote a GDB script instead of using Manticore. I found bit flips that would allow me to bypass both of the checks that would normally prevent the creation of a faulted signature. I used GDB to alter both of those memory instructions. In a process identical to the toy program, I also flipped one bit in a given memory address. I then used Python to loop through each byte of memory, call this script, and try to extract the private keys, again checking whether they were correct by attempting to decrypt a known message. I collected the solved private keys and wrote the results to a CSV file of all the bit flips.

Fig. 4: Excerpt from code to find faultable locations in mbed TLS

Fig. 5: Excerpt from GDB script called from Python code to induce faults in mbed TLS

### Results

I tested 566 bit flips, all within the portion of the mbed TLS code that carried out the signing operation. Combined with the two bit flips that ensured that the checks would pass, I found that 28 of them – nearly 5% – leaked the private keys. About 55% failed to produce a signature.

Fig.6. Bit flip results for mbed TLS

The fact that this kind of analysis works on real programs is exciting, but unfortunately, I ran out of time in the summer before I got a chance to test it in the “real world.” Nonetheless, the ability to input real TLS code and get a comprehensive description of fault attacks against it is exciting, and yields fascinating possibilities for future research.

## Conclusion

I loved working at Trail of Bits. I gained a better understanding of cryptography, and became familiar with some of the tools used by security engineers. It was a wonderful experience, and I’m excited to apply everything I learned to my classes and projects at Carnegie Mellon University when I start next year.

# You could have invented that Bluetooth attack

A serious bluetooth bug has received quite a bit of attention lately. It’s a great find by Biham and Newman. Given BLE’s popularity in the patch-averse IoT world, the bug has serious implications. And yet, it’s remarkably clean and simple. Unlike many elliptic curve bugs, an average human can totally understand the bug and how it can be exploited. It’s a cool application of a conceptually approachable attack.

This post describes the bug, how to exploit them, and how that specifically happened with the bluetooth protocol. But first, let’s take a crash course in elliptic curves and invalid curve point attacks.

## What is an elliptic curve?

It’s quite a misnomer. In cryptography, an “elliptic curve” is neither elliptical nor a continuous curve. Instead, it’s a collection of (x, y) coordinates where x and y are between 0 and n, such that y2 = x3 + ax + b mod n, plus a bonus “point at infinity,” which counterintuitively behaves much like zero; if you add it to anything, you get the same number back. Fig. 1 shows such a curve, where y2 = x3 - x, and x and y range from 0 to 71. (Technically, x and y are defined over a finite field, but all finite fields of the same order are isomorphic, so our definition is equivalent).

Fig. 1: An elliptic curve (as used in cryptography)

Elliptic curves have a few useful properties:

• You can add elliptic curve points to one another with rules that look a lot like regular addition: x + y = y + x, x + (y + z) = (x + y) + z, etc. This is because points on the curve form an Abelian group. You can see a visualization of this addition in fig. 2, below.
• A point can be multiplied by some natural number (call it n) by adding it to itself n times.
• For each point (x, y), there’s an inverse, (x, -y) such that any point plus its inverse is the point at infinity.
• Most notably, if you pick a, b, and n in the equation above well, multiplying by a regular number is a trapdoor function: given a point P and a number n, computing a point Q such that Q = n * P is very easy, but given a point P and a point Q, finding n such that Q = n * P is extremely hard. This simple hardness assumption lets us construct hosts of cryptographic algorithms.

Fig. 2: Addition, and the point at infinity (note: these illustrations use a continuous curve for visualization, but that’s still not what we’re working with)

Usually, elliptic curve algorithms are written around a specific curve. Parties exchange points on the curve and scalars, and do computations like we’ve defined above using them. However, problems arise when these algorithms are exposed to (x, y) pairs that don’t satisfy the curve equation, and these can be exploited to perform what’s called an “invalid curve point attack.”

## What is an invalid curve point attack?

Remember, a point is a pair (x, y) such that y2 = x3 + ax + b mod n for some a, b, and n. However, if that equation doesn’t hold, (x,y) is an invalid curve point. Quite a few cryptographic algorithms ask a user to provide a curve point and, by design, assume the point is valid and the equation holds. Failing to verify that received curve points are on the curve before doing math with them isn’t too far from violating the cryptographic doom principle and has similar consequences.

In elliptic curve schemes, the secret is usually a regular number (remember, finding n such that Q = n * P is the hard problem). When an attacker can send an unvalidated point that’s multiplied by n and see the results, they can exploit that lack of validation to learn the secret key. Frequently, attackers can pick points that belong to a different curve than the algorithm specifies, one with very few points on it.

For instance, an attacker might pick a point not on the curve with a y coordinate of zero. Any point like this must, when added to itself, be equal to the point at infinity. We know this because we calculate inverses by multiplying the y coordinate by negative one, but zero times negative one is zero, and so any point with a y coordinate of zero is its own inverse. Thus when we add it to itself, the result must be the point at infinity.

If the attacker picks a point like this, then by viewing the secret multiplied by some point on that curve, they learn whether the secret is even or odd! The input point was one of the two possible points. Adding it to itself will get the other point. Thus, if the secret is the point entered, the number is odd; otherwise, it’s even. We can submit similar points equal to the point at infinity when multiplied by three to learn the secret mod 3, points equal to the point at infinity when multiplied by five to learn the secret mod 5, and so on until we can just use the Chinese Remainder Theorem to compute the actual secret.

This isn’t the only way to use invalid curve points to find out a secret key, but it’s perhaps the easiest to understand, and has been used in real life to break TLS libraries from Oracle and Google.

While the recent attack on Bluetooth wasn’t quite as simple as the above example, it was conceptually very similar, and used the same technique of small subgroup confinement to achieve key disclosure.

## How did the Bluetooth attack work?

The Bluetooth protocol uses elliptic curve Diffie-Hellman to agree on a shared secret key for encryption. Using Diffie-Hellman algorithms correctly is super hard. Subtle mistakes can compromise the security of your entire system. In this case, the protocol did in fact require curve point validation, but only for the x coordinate. This is an innocent-enough looking mistake to go unnoticed for a decade. And it lets a smart attacker break the whole system.

Elliptic curve Diffie-Hellman is a simple algorithm. Suppose Alice and Bob want to agree upon some secret. Both parties have a secret number, and there’s a commonly agreed-upon “base point” on some elliptic curve.

Alice sends Bob the base point multiplied by her secret number, and Bob sends Alice the base point multiplied by his. Then, Alice multiplies Bob’s message by her secret number, and Bob multiplies Alice’s message by his secret number. If we call the point P and the secrets a and b, Alice sends Bob P * a, Bob sends Alice P * b. Alice then calculates (P * b) * a (the shared secret) and Bob calculates (P * a) * b (the same number.)

Even if an attacker, Chuck, can see either message, he can’t deduce a or b, and he can’t combine P * a and P * b to get the secret, so he’s totally out of luck! However, problems arise when Chuck can modify messages instead of just viewing them. Since the y coordinate isn’t valid, Chuck can modify it to always be zero.

Remember, if a point has a y coordinate of zero, if you multiply it by a random number, it has a 50% chance of being the point at infinity, a 50% chance of being the original point, and no chance of being anything else.

Putting this all together, if Chuck replaces one of the points Alice and Bob send each other, (x, y), with (x, 0), then Alice or Bob multiplies it by their secret key, there’s a 50% chance they get the point at infinity and a 50% chance they get (x, 0). If Chuck replaces both intermediate messages, there’s a 25% chance that Alice and Bob agree the secret key is the point at infinity, and no chance they agree on any other key. This means either ECDH fails and Alice and Bob have to retry (giving Chuck another chance), or Chuck knows the secret key and can read and insert messages.

## How can you avoid bugs like this?

The most important takeaway from all of this isn’t anything about this particular attack; it’s that this whole class of attacks is totally preventable. A few more concrete pieces of advice:

• Diffie-Hellman is an unusually dangerous algorithm to implement. You almost certainly don’t want to be using it in the first place (ref. Latacora’s excellent cryptographic right answers). If you find someone using it, you have a good chance of finding bugs. Seriously, almost no one needs this, and it’s extraordinarily hard to do right.
• Use X25519 for ECDH or Ed25519 for ECDSA. On those curves any 32-byte string is a valid curve point; invalid curve points are thus impossible.
• If your input can be invalid and you’re performing cryptographic operations with it, do the validation before anything else.

I’ve deliberately left out instructions for validating points yourself, since that’s far too subtle a topic for the conclusion of a blog post. If you’re interested in that sort of thing, you could do worse than this paper. If you’d like to practice exploiting these kind of bugs (and some way cooler ones) you should check out Cryptopals set 8. If this is the kind of thing you do for fun already, get in touch. We’d love to work with you.

# Optimizing Lifted Bitcode with Dead Store Elimination

Tim Alberdingk Thijm

As part of my Springternship at Trail of Bits, I created a series of data-flow-based optimizations that eliminate most “dead” stores that emulate writes to machine code registers in McSema-lifted programs. For example, applying my dead-store-elimination (DSE) passes to Apache httpd eliminated 117,059 stores, or 50% of the store operations to Remill’s register State structure. If you’re a regular McSema user, then pull the latest code to reap the benefits. DSE is now enabled by default.

Now, you might be thinking, “Back it up, Tim, isn’t DSE a fundamental optimization that’s already part of LLVM?” You would be right to ask this (and the answer is yes), because if you’ve used LLVM then you know that it has an excellent optimizer. However, despite LLVM’s excellence, the truth is that, like any optimizer, LLVM can only cut instructions it knows to be unnecessary. The Remill dead code eliminator has the advantage of possessing more higher-level information about the nature of lifted bitcode, which lets it be more aggressive than LLVM in performing its optimizations.

But every question answered just raises more questions! You might now be thinking, “LLVM only does safe optimizations. This DSE is more aggressive… How do we know it didn’t break the lifted httpd program?” Fear not! The dead store elimination tool is specifically designed to perform a whole-program analysis on lifted bitcode that has already been optimized. This ensures that it can find dead instructions with the maximum possible context, avoiding mistakes where the program assumes some code won’t be used. The output is a fully-functioning httpd executable, minus a mountain of useless computation.

## What Happens When We Lift

The backbone of Remill/McSema’s lifted bitcode is the State structure, which models the machine’s register state. Remill emulates reads and writes to registers by using LLVM load and store instructions that operate on pointers into the State structure. Here’s what Remill’s State structure might look like for a toy x86-like architecture with two registers: eax and ebx.

struct State {
uint32_t eax;
uint32_t ebx;
};


This would be represented in LLVM as follows:

%struct.State = type { i32, i32 }


Let’s say we’re looking at a few lines of machine code in this architecture:

mov eax, ebx


A heavily-simplified version of the LLVM IR for this code might look like this:

The first two lines derive pointers to the memory backing the emulated eax and ebx registers (%eax_addr and %ebx_addr, respectively) from a pointer to the state (%state). This derivation is performed using the getelementptr instruction, and is equivalent to the C code &(state->eax) and &(state->ebx). The next two lines represent the mov instruction, where the emulated ebx register is read (load), and the value read is then written to (store) the emulated eax register. Finally, the last three lines represent the add instruction.

We can see that %ebx_0 is stored to %eax_ptr and then %eax_0 is loaded from the %eax_ptr without any intervening stores to the %eax_ptr pointer. This means that the load into %eax_0 is redundant. We can simply use %ebx_0 anywhere that %eax_0 is used, i.e. forward the store to the load.

Next, we might also notice that the store %ebx_0, %eax_ptr instruction isn’t particularly useful either, since store %eax_1, %eax_ptr happens before %eax_ptr is read from again. In fact, this is a dead store. Eliminating these kinds of dead stores is what my optimization focuses on!

This process will go on in real bitcode until nothing more can be forwarded or killed.

So now that you have an understanding of how dead store elimination works, let’s explore how we could teach this technique to a computer.

As it turns out, each of the above steps are related to data-flow analyses. To build our eliminator, we’re going to want to figure out how to represent these decisions using data-flow techniques.

## Building the Eliminator

With introductions out of the way, let’s get into how this dead code elimination is supposed to work.

### Playing the Slots

The DSE pass needs to recognize loads/stores through %eax_ptr and %ebx_ptr as being different. The DSE pass does this by chopping up the State structure into “slots”, which roughly represent registers, with some small distinctions for cases where we bundle sequence types like arrays and vectors as one logical object. The slots for our simplified State structure are:

After chopping up the State structure, the DSE pass tries to label instructions with the slot to which that instruction might refer. But how do we even do this labelling? I mentioned earlier that we have deeper knowledge about the nature of lifted bitcode, and here’s where we get to use it. In lifted bitcode, the State structure is passed into every lifted function as an argument. Every load or store to an emulated register is therefore derived from this State pointer (e.g. via getelementptr, bitcast, etc.). Each such derivation results in a new pointer that is possibly offsetted from its base. Therefore, to determine the slot referenced by any given pointer, we need to calculate that pointer’s offset, and map the offset back to the slot. If it’s a derived pointer, then we need to calculate the base pointer’s offset. And if the base pointer is derived then… really, it’s just offsets all the way down.

### And They Were Slot-mates!

The case that interests us most is when two instructions get friendly and alias to the same slot. That’s all it takes for one instruction to kill another: in Remill, it’s the law of the jungle.

To identify instructions which alias, we use a ForwardAliasVisitor (FAV). The FAV keeps track of all the pointers to offsets to the state structure and all the instructions involving accesses to the state structure in two respective maps. As the name implies, it iterates forward through the instructions it’s given, keeping a tally if it notices that one of the addresses it’s tracking has been modified or used.

Here’s how this information is built up from our instructions:

Each time the FAV visits an instruction, it checks if updates need to be made to its maps.

The accesses map stores the instructions which access state offsets. We’ll use this map later to determine which load and store instructions could potentially alias. You can already see here that the offsets of three instructions are all the same: a clear sign that we can eliminate instructions later!

The offsets map ensures the accesses map can get the right information. Starting with the base %state pointer, the offsets map accumulates any pointers that may be referenced as the program runs. You can think of it as the address book which the loads and stores use to make calls to different parts of the state structure.

The third data structure shown here is the exclude set. This keeps track of all the other values instructions might refer to that we know shouldn’t contact the state structure. These would be the values read by load instructions, or pointers to alloca’d memory. In this example, you can also see that if a value is already in the offsets map or exclude set, any value produced from one such value will remain in the same set (e.g. %eax_1 is excluded since %eax_0 already was). You can think of the exclude set as the Do-Not-Call list to the offset map’s address book.

The FAV picks through the code and ensures that it’s able to visit every instruction of every function. Once it’s done, we can associate the relevant state slot to each load and store as LLVM metadata, and move on to the violent crescendo of the dead code eliminator: eliminating the dead instructions!

### You’ll Be Stone Dead In a Moment

Now it’s time for us to pick through the aliasing instructions and see if any of them can be eliminated. We have a few techniques available to us, following a similar pattern as before. We’ll look through the instructions and determine their viability for elimination as a data-flow.

Sequentially, we run the ForwardingBlockVisitor to forward unnecessary loads and stores and then use the LiveSetBlockVisitor to choose which ones to eliminate. For the purpose of this post, however, we’ll cover these steps in reverse order to get a better sense of why they’re useful.

#### Live and Set Live

The LiveSetBlockVisitor (LSBV) has the illustrious job of inspecting each basic block of a module’s functions to determine the overall liveness of slots in the State. Briefly, live variable analysis allows the DSE to check if a store will be overwritten (“killed”) before a load accesses (“revives”) the slot. The LiveSet of LSBV is a bitset representing the liveness of each slot in the State structure: if a slot is live, the bit in the LiveSet corresponding to the slot’s index is set to 1.

The LSBV proceeds from the terminating blocks (blocks ending with ret instructions) of the function back to the entry block, keeping track of a live set for each block. This allows it to determine the live set of preceding blocks based on the liveness of their successors.

Here’s an example of how an LSBV pass proceeds. Starting from the terminating blocks, we iterate through the block’s instructions backwards and update its live set as we do. Once we’re finished, we add the block’s predecessors to our worklist and continue with them. After analyzing the entry block, we finish the pass. Any stores visited while a slot was already dead can be declared dead stores, which we can then remove.

In order to avoid any undefined behaviour, the LSBV had a few generalizations in place. Some instructions, like resume or indirectbr, that could cause uncertain changes to the block’s live set conservatively mark all slots as live. This provides a simple way of avoiding dangerous eliminations and an opportunity for future improvements.

#### Not To Be Forward, But…

Our work could end here with the LSBV, but there are still potential improvements we can make to the DSE. As mentioned earlier, we can “forward” some instructions by replacing unnecessary sequences of storing a value, loading that value and using that value with direct use of the value prior to the store. This is handled by the ForwardingBlockVisitor, another backward block visitor. Using the aliases gathered by the FAV, it can iterate through the instructions of the block from back to front, keeping track of the upcoming loads to each slot of the State. If we find an operation occurs earlier that accesses the same slot, we can forward it to cut down on the number of operations, as shown in the earlier elimination example.

Doing this step before the LSBV pass allows the LSBV to identify more dead instructions than before. Looking again at our example, we’ve now set up another store to be killed by the LSBV pass. This type of procedure allows us to remove more instructions than before by better exploiting our knowledge of when slots will be used next. Cascading eliminations this way is part of what allows DSE to remove so many instructions: if a store is removed, there may be more instructions rendered useless that can also be eliminated.

## A DSE Diet Testimonial

Thanks to the slimming power of dead store elimination, we can make some impressive cuts to the number of instructions in our lifted code.

For an amd64 Apache httpd, we were able to generate the following report:

Candidate stores: 210,855
Instructions removed from DSE: 273,322
Forwarded stores: 2,222
Perfectly forwarded: 2,836
Forwarded by truncation: 215
Forwarded by casting: 11
Forwarded by reordering: 61
Could not forward: 1,558
Unanalyzed functions: 0

An additional feature of the DSE is the ability to generate DOT diagrams of the instructions removed. Currently, the DSE will produce three diagrams for each function visited, showing the offsets identified, the stores marked for removal, and the post-removal instructions.

DOT diagrams are produced that show eliminated instructions

## Still Hungry for Optimizations?

While this may be the end of Tim’s work on the DSE for the time being, future improvements are already in the pipeline to make Remill/McSema’s lifted bitcode even leaner. Work will continue to handle cases that the DSE is currently not brave enough to take on, like sinking store instructions when a slot is only live down one branch, handling calls to other functions more precisely, and lifting live regions to allocas to benefit from LLVM’s mem2reg pass.

Think what Tim did was cool? Check out the “intern project” GitHub issue tags on McSema and Remill to get involved, talk to us on #binary-lifting channel of the Empire Hacking Slack, or reach out to us via our careers page.

Tim is starting a PhD in programming language theory this September at Princeton University, where he will try his hand at following instructions, instead of eliminating them.

# Trail of Bits donates $100,000 to support young researchers through SummerCon We have a soft spot in our hearts for SummerCon. This event, the longest-running hacker conference in the US, is a great chance to host hacker friends from around the world in NYC, catch up in person, and learn about delightfully weird security topics. It draws a great crowd, ranging from “hackers to feds to convicted felons to concerned parents.” The folks running SummerCon have pulled together an excellent line-up of high-quality talks time and again. However, this year there’s a bigtime issue: all the speakers are men. We recognize the thanklessness of the job of hosting SummerCon and assume the best of intentions. Nonetheless, we were disappointed. This lineup isn’t an exception to security conferences – it’s close to the norm. Exclusion of women and minorities in the security industry is a pandemic that we need to address. The hacker conference that started them all should be at the forefront of the solution. This year we’ll be working together to change that. ## A grant for inclusion in security research We are partnering with the SummerCon Foundation to create the Trail of Bits SummerCon Fellowship. This grant will provide$100,000 in funding for budding security researchers. At least 50% of the program spots will be reserved for minority and female-identifying candidates. The organization will reach out directly to women- and minority-serving groups at universities to encourage them to apply (shout out to @MaddieStone for that awesome idea!). Participants will receive grant funding, mentorship from Trail of Bits and the SummerCon Foundation, and an invitation to present their findings at SummerCon after their fellowship.

In addition to this program, SummerCon has committed to a greater level of transparency and representation in its future selection of speakers. They’ll publish well-defined criteria for their CFP. They will identify the SummerCon alumni who comprise their speaker-selection committee. Finally, they will expand the selection team to include 50% minorities and women.

Next, SummerCon has committed to making the conference a safe space of inclusion. They’ve announced and will enforce a clear anti-harassment policy with multiple points of contact for reporting disrespectful behavior. Violators will be kicked out.

Finally, in a small effort to bring more awareness to the change, we have a sweet bonus in store: Keep your eyes peeled for the Trail-of-Bits-sponsored ice cream flavor in a Van Leeuwen ice cream truck outside LittleField. For every scoop sold, we’ll be matching the sales with a donation to Girls Who Code.

Serving up tasty treats for a cause!

## Does it fix the problem?

No. This is a small step. The issue of inclusion within security is much bigger than one small annual hacker meetup. Fortunately, everyone in the industry can help, including us. Even today, our growing team of 37 people has only four women, only two of whom are engineers. We must do better.

We’ve already taken some steps to improve:

Here’s what we’ll do this year:

• Actively work with diversity- and inclusion-recruiting groups to get out of the cycle of predisposing our recruiting toward homogeneity
• Continue to search for opportunities to volunteer and mentor with groups that support inclusion in tech and infosec
• Reimburse employees for any tax expenses incurred for insurance of domestic partners

## Get involved!

Want to participate as a SummerCon research fellow? Keep an eye on @trailofbits. We’ll be making a joint announcement with SummerCon soon.

# Announcing the Trail of Bits osquery support group

As great as it is, osquery could be a whole lot better. (Think write access for extensions, triggered responses upon detection, and even better performance, reliability and ease of use.)

Facebook’s small osquery team can’t respond to every request for enhancement. That’s understandable. They have their hands full with managing the osquery community, reviewing PRs, and ensuring the security of the world’s largest social network. It’s up to the community to move the osquery platform forward.

Good news: none of these feature requests are infeasible. The custom engineering is just uneconomical for individual organizations to bankroll.

We propose a strategy for osquery users to share the cost of development. Participating companies could pool resources and collectively target specific features. This would accelerate the depreciation of other full-suite tools that are more expensive, less flexible and less transparent.

It’s the only way to make real progress quickly. Otherwise, projects rely solely on the charity and coordination of their contributors.

## Can an open-source tool replace commercial solutions?

We think that open-source security solutions are inherently better. They’re transparent. They’re more flexible. Their costs are tied closely to the value you get; not just access. Finally, each time there’s an investment in the tool, it increases the advantages for current users, and increases the number of users who can access these advantages.

However, in order to compete with their commercial counterparts, open source projects need implementation support and development support. The former is basically the ability to “set it and forget it.” The latter ensures the absence of show-stopping bugs and the regular addition of new required features.

Companies like Kolide and Uptycs provide user-friendly support for deployment.

For development support, you can now hire us.

## Announcing the Trail of Bits osquery support group

We’re offering two ‘flavors’ of support plans; one for year-round assurance, the other for custom development.

### 12-month assurance plan

Think of this like an all-you-can-eat buffet for critical features and fixes. Any time you need a bug fixed or a feature added, just file a ticket with us. This option’s great for root-cause and fix issues, the development of new tables and extensions, or the redesign of parts of osquery’s core. Basically, the stuff that is holding you back from cancelling those expensive monthly contracts with the proprietary vendors.

### Bespoke development

This plan’s for you if you need one-off help with a big-time osquery change. Perhaps: ports to new platforms, non-core features, or forks.

Regardless of the plan you choose, you’ll get:

• The opportunity to participate in a bi-weekly iteration planning meeting for collaborative feature ideation, problem-solving, and feature prioritization
• A private GitHub repository with issue tracker for visibility and influence over what features are worked on
• Special access and support to our osquery extensions

Whether you’re a long-time osquery user with a list of feature requests, or part of a team that has been holding out for osquery’s feature-parity with commercial tools, this may be the opportunity you’ve been waiting for. As a member, you’ll gain multiple benefits: confidence that there aren’t any show-stopping bugs; direct access to our team of world-class engineers, many of whom have been doing this exact work since we ported osquery to Windows; peace of mind that your internal engineers won’t spend any more time on issues with osquery; and the chance to drive osquery’s product direction while leaving the heavy lifting to us.

Want in? Let us know.

# QueryCon 2018: our talks and takeaways

Sometimes a conference just gets it right. Good talks, single track, select engaged attendees, and no sales talks. It’s a recipe for success that Kolide got right on its very first try with QueryCon, the first-ever osquery conference.

It’s no secret that we are huge fans of osquery, Facebook’s award-winning open source endpoint detection tool. From when we ported osquery to Windows in 2016 to our launch of our osquery extension repo this year, we’ve been one of the leading contributors to the tool’s development. This is why we were delighted Kolide invited us to participate in QueryCon!

The two-day conference, hosted at the beautiful Palace of the Fine Arts in San Francisco, drew over 120 attendees and 16 speakers. The attendance list was a Who’s Who in Big Tech security; teams from Facebook, Airbnb, Yelp, Atlassian, Adobe, Netflix, Salesforce, and more. It was great to meet face-to-face. We’ve been collaborating with some of these teams on osquery for years. It was also exciting to see the widespread adoption of the technology manifested in person. Though some of the teams attending were there to learn about the tech before deploying, the majority seemed to be committed adopters.

The talks ranged from the big-picture (operational security preparedness by Rob Fry of JASK) to the highly technical (breakdowns of macOS internals by Michael Lynn of Facebook), with consistent levity, epitomized by the brilliantly sulky Ben Hughes of Stripe. Scott Lundgren of Carbon Black gave a report-card-style review of the community from an outsider’s perspective. Longtime osquery evangelist Chris Long of Palantir provided a candid user experience of working with osquery’s audit framework in his organization. It was a well-curated mix of subjects, speakers, and perspectives. They all taught us something new.

## What we learned at QueryCon

### 1. The community is bigger and stronger than we thought

As of this week, osquery’s Slack has 1,703 users. Until the sold-out showing at QueryCon, I never thought to check how many of those users were active; 431 in the last 30 days. 120 of those people made it to QueryCon. Dozens more joined the waitlist.

### 2. Some users are innovating in very cool ways

We came to QueryCon intent on pushing the community to use osquery in new, innovative ways. Turns out, it didn’t need much pushing. Take the security team at Netflix. They’re using osquery in multiple internal open source projects: Diffy, a digital forensics and incident response (DFIR) tool, and Stethoscope, their security detection and recommendation application. We heard many more examples from many more teams.

### 3. The community really likes our contributions

Many of the talks mentioned our team and our work. We knew we were contributing significant engineering effort, but we hadn’t truly realized how much others had been benefiting. It felt great to hear that work done for our clients truly advances the whole community.

### 4. The goals are clear, but the way there is not

We gleaned some clear takeaways that are likely common for a first meetup of a new open source project:

• We need to define and broadcast osquery’s guiding principles;
• We need to solidify some best practices for effective collaboration;
• We need to tackle technical debt.

However, we didn’t determine how these will get done. Facebook was clear in defining its role in this process. Their small dedicated osquery team will continue to put in the hard work of testing, managing versions, and holding the community to high standards for both written code and community inclusion. However, it’s up to the community to take care of the rest.

## What we shared at QueryCon

### Osquery Super Features

Speaker: Lauren Pearl

Abstract: In this talk, we reviewed a user feature wishlist gathered from interviews with five Silicon Valley tech teams who use osquery. From these, we identified Super Features – features that would fundamentally improve the value proposition of osquery. We explained how these developments could transform osquery’s power in technical organizations. Finally, we walked through the high-level development plans for making these Super Features a reality.

Slides: Super Features PDF

### The Osquery Extensions Skunkworks Project: Unconventional Uses for Osquery

Speaker: Mike Myers

Abstract: Facebook created osquery with certain guiding principles: don’t pry into users’ data, don’t change the state of the system, don’t create network traffic to third parties. It was originally intended as a read-only information gatherer. For those that didn’t want to play by these rules, there’s the extension interface. We’ve begun experimenting with extensions that don’t align with mainline osquery: integrating with third-party services, writable tables, host-based firewall administration, malware vaccination, and more. We shared some of our lessons-learned on the challenges of using osquery as a control interface.

Slides: Skunkworks Extensions PDF

## Thank you so much!

This was a great first conference for an emerging technology. It awakened community leaders to issues and opportunities and started the conversation of how to push forward. Attendees renewed enthusiasm and commitment to advance and maintain the project.

It’s hard to believe that this was Kolide’s first time hosting such an event. Director Of Operations, Antigoni Sinanis, the lady in charge of the event’s success, has set a high bar for her company to clear next year. We at are already looking forward to round two!

# Manage your fleet’s firewalls with osquery

Each of the three major operating systems provides a native firewall, capable of blocking incoming and outgoing access when configured. However, the interface for each of these three firewall systems are dissimilar and each requires different methods of configuration. Furthermore, there are few options for cross-platform fleet configuration, and nearly all are commercial and proprietary.

In partnership with Airbnb, we have created a cross-platform firewall management extension for osquery. The extension enables programmatic control over the native firewalls and provides a common interface for each host operating system, permitting more advanced control over an enterprise fleet’s endpoint protections as well as closing the loop between endpoint monitoring and endpoint management.

Along with our Santa management extension, this extension shows the utility of writable tables in osquery extensions. Programmatic control over endpoint firewalls means that an administrator can react more quickly to prevent the spread of malware on their fleet, prevent unexpected data egress from particularly vital systems, or block incoming connections from known malicious addresses. This is a huge advance in osquery’s capabilities, shifting it from merely a monitoring tool into both prevention and recovery domains.

## What it can do now

The extension creates two new tables: HostBlacklist and PortBlacklist. These virtual tables generate their entries via the underlying operating systems’ native firewall interfaces: iptables on Linux, netsh on Windows, and pfctl on MacOS. This keeps them compatible with the widest possible range of deployments and avoids further dependence on external libraries or applications. It will work with your existing configuration, and, regardless of underlying platform, provide the same interface and capabilities.

Use osquery to access the local firewall configuration on Mac, Windows, and Linux

## What’s on the horizon

While the ability to read the state of the firewall is useful, it’s the possibility of controlling them that we’re most excited about. With writable tables available in osquery, blacklisting a port or a host on a managed system will become as simple as an INSERT statement. No need to deploy an additional firewall management service. No more reviewing how you configure the firewall on macOS. Just write an INSERT statement and push it out the fleet.

Instantly block hostnames and ports across your entire fleet with osquery

## Give it a try

With this extension you can query the state of blacklisted ports and hosts across a managed fleet and ensure that they’re all configured to your specifications. With the advent of the writable tables feature osquery can shift from a monitoring role to a management and preventative tool. This extension takes the first step in that direction.

We’re adding this extension to our managed repository. We’re committed to maintaining and extending our collection of extensions. You should check in and see what else we’ve released.

Do you have an idea for an osquery extension? File an issue on our GitHub repo for it. Contact us for osquery development.

# Manage Santa within osquery

We’re releasing an extension for osquery that lets you manage Google Santa without the need for a separate sync server.

Google Santa is an application whitelist and blacklist system for macOS ideal for deployment across managed fleets. It uses a sync server from which daemons pull rules onto managed computers. However, the sync server provides no functionality for the bulk collection of logs or configuration states. It does not indicate whether all the agents have pulled the latest rules or how often those agents block execution of blacklisted binaries.

In partnership with Palantir, we have integrated Santa into the osquery interface as an extension. Santa can now be managed directly through osquery and no longer requires a separate sync server. Enterprises can use a single interface, osquery, to centrally manage logs and update or review agent configuration.

We’ve described writable access to endpoints as a superfeature of osquery. This extension shows why. Now, it’s possible to add remote management features to the osquery agent, which is normally limited to read-only access. This represents a huge advance in osquery’s capabilities, moving it from the role of strictly monitoring into an active and preventative role. Trail of Bits is pleased to announce the release of the Santa extension into our open-source repository of osquery extensions.

## What it can do

Santa gives you fine-grained control over which applications may run on your computer. Add osquery and this extension into the mix, and now you’ve got fine-grained control over which applications may run on your fleet. Lock down endpoints to only run applications signed by a handful of approved certificates, or blacklist known malicious applications before they get a chance to run.

The extension can be loaded at the startup of osquery with the extension command line argument, e.g., osqueryi --extension path/to/santa.ext. On loading, it adds two new tables to the database: santa_rules and santa_events.The tables themselves are straightforward.

santa_rules consists of the three text columns: shasum, state, and type. The type column contains the rule type and may be either certificate or binary. state is either whitelist or blacklist. shasum contains either the hash of the binary or the signing certificate’s hash, depending on rule type.

The santa_events table has four text columns: timestamp, path, shasum, and reason. timestamp marks the time the deny event was logged. path lists the path to the denied application. shasum displays the hash of the file. reason shows the type of rule that caused the deny (either binary or certificate).

## Time to use it

This extension provides a simplified interface to oversee and control your Santa deployment across your fleet, granting easy access to both rules and events. You can find it and other osquery extensions in our repository of maintained osquery extensions. We’ll continue to add new extensions. Take a look and see what we have available.

## Hire us to tailor osquery to your needs

Do you have an idea for an osquery extension? File an issue on our GitHub repo for it. Contact us for osquery development.

Note: This feature depends on writable tables support for extensions which has not yet been merged. Contact us if you’d like to try this feature now — we create custom binary builds to test upcoming features of osquery for our clients.

# Collect NTFS forensic information with osquery

We’re releasing an extension for osquery that will let you dig deeper into the NTFS filesystem. It’s one more tool for incident response and data collection. But it’s also an opportunity to dispense with forensics toolkits and commercial services that offer similar capabilities.

Until now, osquery has been inadequate for performing the kind of filesystem forensics that is often part of an incident response effort. It collects some information about files on its host platforms – timestamps, permissions, owner and more – but anyone with experience in forensics will tell you that there’s a lot more data available on a file system if you’re willing to dig. Think additional timestamps, unallocated metadata, or stale directory entries.

The alternatives are often closed source and expensive. They become one more item in your budget, deployment roadmap, and maintenance schedule. And none of them integrate with osquery. You have to go to the extra effort of mapping the forensic report back to your fleet.

That changes today. In partnership with Crypsis, we have integrated NTFS forensic information into the osquery interface as an extension. Consider this the first step toward a better, cost-effective, more efficient alternative that’s easier to deploy.

## What it can do

The NTFS forensics extension provides specific additional file metadata from NTFS images, including filename timestamp entries, the security descriptor for files, whether a file has Alternate Data Streams (ADS), as well as other information. It also provides index entries for directory indices, including entries that are deallocated. You can find the malware that just cleaned up after itself, or altered its file timestamps but forgot about the filename timestamps, or installed a rootkit in the ADS of calc.exe, all without ever leaving osquery.

## How to use it

Load the extension at the startup of osquery with the command line argument, e.g., <code>osqueryi.exe --extension path\to\ntfs_forensics.ext.exe</code>. On loading, three new tables will be added to the database: ntfs_part_data, ntfs_file_data, and ntfs_indx_data.

### ntfs_part_data

This table provides information about partitions on a disk image. If queried without a specified disk image, it will attempt to interrogate the physical drives of the host system by walking up from \\.\PhysicalDrive0 until it finds a drive number it fails to open.

Enumerating partition entries in an NTFS image

### ntfs_file_data

This table provides information about file entries in an NTFS file system. The device and partition columns must be specified explicitly in the WHERE clause to query the table. If the path or inode column is specified, then a single row about the specified file is returned. If the directory column is specified, then a row is returned for every file in that directory. If nothing is specified, a walk of the entire partition is performed. Because the walk of the entire partition is costly, results are cached to be reused without reperforming the entire walk. If you need fresh results of a partition walk, use the hidden column from_cache in the WHERE clause to force the collection of live data (e.g., select * from ntfs_file_data where device=”\\.\PhysicalDrive0” and partition=2 and from_cache=0;).

Displaying collected data on a single entry in an NTFS file system

### ntfs_indx_data

This table provides the content of index entries for a specified directory, including index entries discovered in slack space. Like ntfs_file_data, the device and partition columns must be specified in the WHERE clause of a query, as well as either parent_path or parent_inode. Entries discovered in slack space will have a non-zero value in the slack column.

Displaying inode entries recovered from a directory index’s slack space

### Getting Started

This extension offers a fast and convenient way to perform filesystem forensics on Windows endpoints as a part of an incident response. You can find it and our other osquery extensions in our repository. We’re committed to maintaining and extending our collection of extensions. Take a look, and see what else we have available.

## Hire us to tailor osquery to your needs

Do you have an idea for an osquery extension? File an issue on our GitHub repo for it. Contact us for osquery development.

# State Machine Testing with Echidna

Property-based testing is a powerful technique for verifying arbitrary properties of a program via execution on a large set of inputs, typically generated stochastically. Echidna is a library and executable I’ve been working on for applying property-based testing to EVM code (particularly code written in Solidity).

Echidna is a library for generating random sequences of calls against a given smart contract’s ABI and making sure that their evaluation preserves some user-defined invariants (e.g.: the balance in this wallet must never go down). If you’re from a more conventional security background, you can think of it as a fuzzer, with the caveat that it looks for user-specified logic bugs rather than crashes (as programs written for the EVM don’t “crash” in any conventional way).

The property-based testing functionality in Echidna is implemented with Hedgehog, a property-based testing library by Jacob Stanley. Think of Hedgehog as a nicer version of QuickCheck. It’s an extremely powerful library, providing automatic minimal testcase generation (“shrinking”), well-designed abstractions for things like ranges, and most importantly for this blog post, abstract state machine testing tools.

After reading a particularly excellent blog post by Tim Humphries (“State machine testing with Hedgehog,” which I’ll refer to as the “Hedgehog post” from now on) about testing a simple state machine with this functionality, I was curious if the same techniques could be extended to the EVM. Many contracts I see in the wild are just implementations of some textbook state machine, and the ability to write tests against that invariant-rich representation would be invaluable.

The rest of this blog post assumes at least a degree of familiarity with Hedgehog’s state machine testing functionality. If you’re unfamiliar with the software, I’d recommend reading Humphries’s blog post first. It’s also worth noting that the below code demonstrates advanced usage of Echidna’s API, and you can also use it to test code without writing a line of Haskell.

First, we’ll describe our state machine’s states, then its transitions, and once we’ve done that we’ll use it to actually find some bugs in contracts implementing it. If you’d like to follow along on your own, all the Haskell code is in examples/state-machine and all the Solidity code is in solidity/turnstile.

## Step 0: Build the model

Fig. 1: A turnstile state machine

The state machine in the Hedgehog post is a turnstile with two states (locked and unlocked) and two actions (inserting a coin and pushing the turnstile), with “locked” as its initial state. We can copy this code verbatim.

data ModelState (v :: * -> *) = TLocked
| TUnlocked
deriving (Eq, Ord, Show)

initialState :: ModelState v
initialState = TLocked


However, in the Hedgehog post the effectful implementation of this abstract model was a mutable variable that required I/O to access. We can instead use a simple Solidity program.

contract Turnstile {
bool private locked = true; // initial state is locked

function coin() {
locked = false;
}

function push() returns (bool) {
if (locked) {
return(false);
} else {
locked = true;
return(true);
}
}
}


At this point, we have an abstract model that just describes the states, not the transitions, and some Solidity code we claim implements a state machine. In order to test it, we still have to describe this machine’s transitions and invariants.

## Step 1: Write some commands

To write these tests, we need to make explicit how we can execute the implementation of our model. The examples given in the Hedgehog post work in any MonadIO, as they deal with IORefs. However, since EVM execution is deterministic, we can work instead in any MonadState VM.

The simplest command is inserting a coin. This should always result in the turnstile being unlocked.

s_coin :: (Monad n, MonadTest m, MonadState VM m) => Command n m ModelState
s_coin = Command (\_ -> Just $pure Coin) -- Regardless of initial state, we can always insert a coin (\Coin -> cleanUp >> execCall ("coin", [])) -- Inserting a coin is just calling coin() in the contract -- We need cleanUp to chain multiple calls together [ Update$ \_ Coin _ -> TUnlocked
-- Inserting a coin sets the state to unlocked
, Ensure $\_ s Coin _ -> s === TUnlocked -- After inserting a coin, the state should be unlocked ]  Since the push function in our implementation returns a boolean value we care about (whether or not pushing “worked”), we need a way to parse EVM output. execCall has type MonadState VM => SolCall -> m VMResult, so we need a way to check whether a given VMResult is true, false, or something else entirely. This turns out to be pretty trivial. match :: VMResult -> Bool -> Bool match (VMSuccess (B s)) b = s == encodeAbiValue (AbiBool b) match _ _ = False  Now that we can check the results of pushing, we have everything we need to write the rest of the model. As before, we’ll write two Commands; modeling pushing while the turnstile is locked and unlocked, respectively. Pushing while locked should succeed, and result in the turnstile becoming locked. Pushing while unlocked should fail, and leave the turnstile locked. s_push_locked :: (Monad n, MonadTest m, MonadState VM m) => Command n m ModelState s_push_locked = Command (\s -> if s == TLocked then Just$ pure Push else Nothing)
-- We can only run this command when the turnstile is locked
(\Push -> cleanUp >> execCall ("push", []))
-- Pushing is just calling push()
[ Require $\s Push -> s == TLocked -- Before we push, the turnstile should be locked , Update$ \_ Push _ -> TLocked
-- After we push, the turnstile should be locked
, Ensure $\before after Push b -> do before === TLocked -- As before assert (match b False) -- Pushing should fail after === TLocked -- As before ]  s_push_unlocked :: (Monad n, MonadTest m, MonadState VM m) => Command n m ModelState s_push_unlocked = Command (\s -> if s == TUnlocked then Just$ pure Push else Nothing)
-- We can only run this command when the turnstile is unlocked
(\Push -> cleanUp >> execCall ("push", []))
-- Pushing is just calling push()
[ Require $\s Push -> s == TUnlocked -- Before we push, the turnstile should be unlocked , Update$ \_ Push _ -> TLocked
-- After we push, the turnstile should be locked
actions <- forAll $Gen.sequential (Range.linear 1 100) initialState [s_coin, s_push_locked, s_push_unlocked -- Generate between 1 and 100 actions, starting with a locked (model) turnstile evalStateT (executeSequential initialState actions) v -- Execute them sequentially on the given VM.  You can think of the above code as a function that takes an EVM state and returns a hedgehog-checkable assertion that it implements our (haskell) state machine definition. ## Step 3: Test With this property written, we’re ready to test some Solidity! Let’s spin up ghci to check this property with Echidna. λ> (v,_,_) <- loadSolidity "solidity/turnstile/turnstile.sol" -- set up a VM with our contract loaded λ> check$ prop_turnstile v -- check that the property we just defined holds
✓ passed 10000 tests.
True
λ>


It works! The Solidity we wrote implements our model of the turnstile state machine. Echidna evaluated 10,000 random call sequences without finding anything wrong.

Now, let’s find some failures. Suppose we initialize the contract with the turnstile unlocked, as below. This should be a pretty easy failure to detect, since it’s now possible to push successfully without putting a coin in first.

We can just slightly modify our initial contract as below:

contract Turnstile {
bool private locked = false; // initial state is unlocked

function coin() {
locked = false;
}

function push() returns (bool) {
if (locked) {
return(false);
} else {
locked = true;
return(true);
}
}
}


And now we can use the exact same ghci commands as before:

λ> (v,_,_) <- loadSolidity "solidity/turnstile/turnstile_badinit.sol"
λ> check $prop_turnstile v ✗ failed after 1 test. ┏━━ examples/state-machine/StateMachine.hs ━━━ 49 ┃ s_push_locked :: (Monad n, MonadTest m, MonadState VM m) => Command n m ModelState 50 ┃ s_push_locked = Command (\s -> if s == TLocked then Just$ pure Push else Nothing)
51 ┃   (\Push -> cleanUp >> execCall ("push", []))
52 ┃   [ Require $\s Push -> s == TLocked 53 ┃ , Update$ \_ Push _ -> TLocked
54 ┃   , Ensure $\before after Push b -> do before === TLocked 55 ┃ assert (match b False) ┃ ^^^^^^^^^^^^^^^^^^^^^^ 56 ┃ after === TLocked 57 ┃ ] ┏━━ examples/state-machine/StateMachine.hs ━━━ 69 ┃ prop_turnstile :: VM -> property 70 ┃ prop_turnstile v = property$ do
71 ┃   actions <- forAll $Gen.sequential (Range.linear 1 100) initialState 72 ┃ [s_coin, s_push_locked, s_push_unlocked] ┃ │ Var 0 = Push 73 ┃ evalStateT (executeSequential initialState actions) v This failure can be reproduced by running: > recheck (Size 0) (Seed 3606927596287211471 (-1511786221238791673)) False λ>  As we’d expect, our property isn’t satisfied. The first time we push it should fail, as the model thinks the turnstile is locked, but it actually succeeds. This is exactly the result we expected above! We can try the same thing with some other buggy contracts as well. Consider the below Turnstile, which doesn’t lock after a successful push. contract Turnstile { bool private locked = true; // initial state is locked function coin() { locked = false; } function push() returns (bool) { if (locked) { return(false); } else { return(true); } } }  Let’s use those same ghci commands one more time λ> (v,_,_) <- loadSolidity "solidity/turnstile/turnstile_nolock.sol" λ> check$ prop_turnstile v
✗ failed after 4 tests and 1 shrink.

┏━━ examples/state-machine/StateMachine.hs ━━━
50 ┃ s_push_locked = Command (\s -> if s == TLocked then Just $pure Push else Nothing) 51 ┃ (\Push -> cleanUp >> execCall ("push", [])) 52 ┃ [ Require$ \s Push -> s == TLocked
53 ┃   , Update $\_ Push _ -> TLocked 54 ┃ , Ensure$ \before after Push b -> do before === TLocked
55 ┃                                         assert (match b False)
┃                                         ^^^^^^^^^^^^^^^^^^^^^^
56 ┃                                         after === TLocked
57 ┃  ]

┏━━ examples/state-machine/StateMachine.hs ━━━
69 ┃ prop_turnstile :: VM -> property
70 ┃ prop_turnstile v = property \$ do
72 ┃   [s_coin, s_push_locked, s_push_unlocked]
┃   │ Var 0 = Coin
┃   │ Var 1 = Push
┃   │ Var 3 = Push
73 ┃   evalStateT (executeSequential initialState actions) v

This failure can be reproduced by running:
> recheck (Size 3) (Seed 133816964769084861 (-8105329698605641335))

False
λ>


When we insert a coin then push twice, the second should fail. Instead, it succeeds. Note that in all these failures, Echidna finds the minimal sequence of actions that demonstrates the failing behavior. This is because of Hedgehog’s shrinking features, which provide this behavior by default.

More broadly, we now have a tool that will accept arbitrary contracts (that implement the push/coin ABI), check whether they implement our specified state machine correctly, and return either a minimal falsifying counterexample if they do not. As a Solidity developer working on a turnstile contract, I can run this on every commit and get a simple explanation of any regression that occurs.

## Concluding Notes

Hopefully the above presents a motivating example for testing with Echidna. We wrote a simple description of a state machine, then tested four different contracts against it; each case yielded either a minimal proof the contract did not implement the machine or a statement of assurance that it did.

If you’d like to try implementing this kind of testing yourself on a canal lock, use this exercise we wrote for a workshop.