Emerging Talent: Winternship 2020 Highlights

The Trail of Bits Winternship is our winter internship program where we invite 10-15 students to join us over the winter break for a short project that has a meaningful impact on information security. They work remotely with a mentor to create or improve tools that solve a single impactful problem. These paid internships give student InfoSec engineers real industry experience, plus a publication for their resumé—and sometimes even lead to a job with us (congrats, Samuel Caccavale!).

Check out the project highlights from some of our 2020 Winternship interns below.

Aaron Yoo—Anvill Decompiler


This winter break I added a tool to the Anvill decompiler that produces “JSON specifications” for LLVM bitcode functions. These bitcode-derived specifications tell Anvill about the physical location (register or memory) of important values such as function arguments and return values. Anvill depends on this location information to intelligently lift machine code into high-quality, easy-to-analyze LLVM bitcode.

A typical specification looks something like this:

    "arch": "amd64",
    "functions": [
            "demangled_name": "test(long, long)",
            "name": "_Z4testll",
            "parameters": [
                    "name": "param1",
                    "register": "RDI",
                    "type": "l"

Overall, I had fun learning so much about ABIs and using the LLVM compiler infrastructure. I got to see my tool operate in some sample full “machine code to C” decompilations, and overcame tricky obstacles, such as how a single high-level parameter or return value can be split across many machine-level registers. My final assessment: Decompilers are pretty cool!

Paweł Płatek—DeepState and Python

AGH University of Science and Technology

The main goal of my winternship project was to find and fix bugs in the Python part of the DeepState source code. Most of the bugs I found were making it nearly impossible to build DeepState for fuzzing or to use the fuzzer’s executors. Now, the build process and executors work correctly, and have been tested and better documented. I’ve also identified and described places where more work is needed (in GitHub issues). Here are the details of my DeepState project:

Cmake—Corrected build options; added the option to build only examples; added checks for compilers and support for Honggfuzz and Angora; improved cmake for examples (so the examples are automatically found).

Docker—Split docker build into two parts—deepstate-base and deepstate—to make it easier to update the environment; added multi-stage docker builds (so fuzzers can be updated separately, without rebuilding everything from scratch); added –jobs support and Angora.

CI—Rewrote a job that builds and pushes docker images to use GitHub action that supports caching; added fuzzer tests.

Fuzzer executors (frontends)—Unified arguments and input/output directory handling, reviewed each fuzzer documentation, so executors set appropriate runtime flags, reimplemented pre- and post-execution methods, added methods for fuzzers’ executables discovery (based on FUZZERNAME_HOME environment variables and CLI flag), reimplemented logging, fixed compilation functions, rewritten methods related to fuzzer’s runtime statistics, reimplemented run method (so that the management routine that retrieves statistics & synchronize stuff is called from time to time and that exceptions are handled properly; also added cleanup function and possibility to restart process), examined each fuzzer directory structure and seed synchronization possibilities and, based on that, implemented fuzzers resuming and fixed ensembling methods.

Fuzzer testing—Created a basic test that checks whether executors can compile correctly and whether fuzzers can find a simple bug; created test for seed synchronization.

Documentation—Split documentation into several files, and added chapters on fuzzer executor usage and harness writing.

Philip Zhengyuan Wang—Manticore

University of Maryland

During my winternship, I helped improve Manticore’s versatility and functionality. Specifically, I combined it with Ansible (an automated provisioning framework) and Protobuf (a serialization library) to allow users to run Manticore in the cloud and better understand what occurs during a Manticore run.

As it stands, Manticore is very CPU-intensive; it competes for CPU time with other user processes when running locally. Running a job on a remotely provisioned VM in which more resources could be diverted to a Manticore run would make this much less of an issue.

To address this, I created “mcorepv” (short for Manticore Provisioner), a Python wrapper for Manticore’s CLI and Ansible/DigitalOcean that allows users to select a run destination (local machine/remote droplet) and supply a target Manticore Python script or executable along with all necessary runtime flags. If the user decides to run a job locally, mcorepv executes Manticore analysis in the user’s current working directory and logs the results.

Things get more interesting if the user decides to run a job remotely—in this case, mcorepv will call Ansible and execute a playbook to provision a new DigitalOcean droplet, copy the user’s current working directory to the droplet, and execute Manticore analysis on the target script/executable. While the analysis is running, mcorepv streams logs and Manticore’s stdout back in near real time via Ansible so a user may frequently check on the analysis’ progress.

Manticore should also simultaneously stream its list of internal states and their statuses (ready, busy, killed, terminated) to the user via a protobuf protocol over a socket in order to better describe the analysis’ status and resource consumption (this is currently a work in progress). To make this possible, I developed a protobuf protocol to represent Manticore’s internal state objects and allow for serialization, along with a terminal user interface (TUI). Once started on the droplet, Manticore spins up a TCP server that provides a real-time view of the internal state lists. The client can then run the TUI locally, which will connect to the Manticore server and display the state lists. Once the job has finished, the Manticore server is terminated, and the results of the Manticore run along with all logs are copied back to the user’s local machine where they may be further inspected.

There’s still some work to be done to ensure Manticore runs bug-free in the cloud. For example:

  • Port forwarding must be set up on the droplet and local machine to ensure Manticore’s server and client TUI can communicate over SSH.
  • The TUI needs additional optimization and improvement to ensure the user gets the right amount of information they need.
  • Mcorepv and its Ansible backend need to be more rigorously tested to ensure they work properly.

I’m glad that in my short time at Trail of Bits, I was able to help move Manticore one step closer to running anywhere, anytime.

Fig 1: Proof of concept—Manticore TUI displaying a list of state objects and log messages to the user.

Samuel Caccavale—Go

Northeastern University

During my winternship, I developed AST- and SSA-based scanners to find bugs in Go code that were previously overlooked by tools like GoSec and errcheck. One unsafe code pattern targeted was usage of a type assertion value before checking whether the type assertion was ok in value, ok := foo.(). While errcheck will detect type assertions that do not bind the ok value (and therefore cause a panic if the type assertion fails), it can’t exhaustively check whether the usage of value is within a context where ok is true. The example reproduces the most trivial example where errcheck and the SSA approach diverge; the SSA approach will correctly detect the usage of safe as safe, and the usage of unsafe as unsafe:

package main

import ("fmt")

func main() {
    var i interface{} = "foo"

    safe, ok := i.(string)
    if ok {

    unsafe, ok := i.(string)
    if true {

Taylor Pothast—Mishegos

Vanderbilt University

During my winternship, I worked on improving the performance of mishegos, Trail of Bits’ differential fuzzer for x86_64 decoders, by switching the cohort collection and output components from their original proof-of-concept JSON format to a compact binary format.

To do this, I learned about mishegos’ internal workings, its in-memory result representations, binary parsing, and how to write Kaitai Struct definitions. My work was merged on the final day of my internship, and is now the default output format for mishegos runs.

To make my work compatible with mishegos’s preexisting analysis tools, I also added a helper utility, mish2jsonl, for converting the new binary output into a JSON form mostly compatible with the original output format. Finally, I updated the analysis tools to handle the changes I made in the JSON-ified output format, including new symbolic fields for each fuzzed decoder’s state.

Thomas Quig—Crytic and Slither

University of Illinois Urbana-Champaign

While at Trail of Bits, I integrated Slither’s smart contract upgradeability checks into Crytic, Trail of Bits’ CI service for Ethereum security. Because smart contracts are immutable upon upload, users need to be able to upgrade their contracts if they ever need to be uploaded. To resolve this issue, the user can have the old contract, a new contract, and a proxy contract. The proxy contract contains what are essentially function pointers that can be modified to point towards the new contract. Risks arise if the aforementioned process is done incorrectly (e.g., incorrect global variable alignment). With Slither, the user can check to make sure those risks are mitigated.

The integration process was much more complicated than I thought it would be, but I was still able to successfully implement the checks. Learning the codebase and the multiple languages required to work with it simultaneously was quite difficult, but manageable. Crytic now grabs the list of all smart contracts and displays them within settings so they can be chosen. The user can pick which contract is the old contract, the new contract, and the proxy contract. Upgradeability checks are then run on those contracts, and the output is displayed to a new findings page in an easily analyzable JSON format.

I enjoyed my time at Trail of Bits. My mentors helped me learn the infrastructure while giving me opportunities to work independently. I gained significant experience in a short period of time and learned about many topics I didn’t expect to like.

William Wang—OpenSSL and Anselm


This winter I worked on Anselm. OpenSSL is one of the most popular cryptography libraries for developers, but it’s also shockingly easy to misuse. Still, many instances of improper use fall into specific patterns, which is where Anselm comes in. My main goal was to prototype a system for detecting these behaviors.

I spent most of my time writing an LLVM pass to detect OpenSSL API calls and form a simplified graph of nodes representing possible execution paths. In larger codebases, traversing through each individual IR block can be time consuming. By “compressing” the graph to its relevant nodes (API calls) first, Anselm enables more complex analyses on it.

I also explored and began implementing heuristics for bad behaviors of varying complexity. For example, mandating that a cipher context be initialized only involves searching the children of nodes where one is created. Similarly, other ordering requirements can be enforced through the call graph alone. However, a bug like repeated IVs/nonces likely requires argument/return value analysis, which I’d like to research more in the future.

While I’m happy with what I accomplished over the winternship, there’s a lot more to be done. In addition to fleshing out the ideas mentioned above, I’d like to polish up the final interface so other developers can easily write their own heuristics. Working with LLVM IR also means that Anselm can theoretically operate on other languages that use OpenSSL bindings. I’m excited to tackle these and other challenges in the future!

See you in the fall?

We’ve selected our summer 2020 interns, but if you’d like to apply (or suggest an intern) for fall, contact us!

Reinventing Vulnerability Disclosure using Zero-knowledge Proofs

We, along with our partner Matthew Green at Johns Hopkins University, are using zero-knowledge (ZK) proofs to establish a trusted landscape in which tech companies and vulnerability researchers can communicate reasonably with one another without fear of being sabotaged or scorned. Over the next four years, we will push the state of the art in ZK proofs beyond theory, and supply vulnerability researchers with software that produces ZK proofs of exploitability. This research is part of a larger effort funded by the DARPA program Securing Information for Encrypted Verification and Evaluation (SIEVE).

Much recent ZK work has focused on blockchain applications, where participants must demonstrate to the network that their transactions follow the underlying consensus rules. Our work will substantially broaden the types of statements provable in ZK. By the end of the program, users will be able to prove statements about programs that run on an x86 processor.

Why ZK proofs of exploitability?

Software makers and vulnerability researchers have a contentious relationship when it comes to finding and reporting bugs. Disclosing too much information about a vulnerability could ruin the reward for a third-party researcher while premature disclosure of a vulnerability could permanently damage the reputation of a software company. Communication between these parties commonly breaks down, and the technology industry suffers because of it.

Furthermore, in many instances companies are unwilling to engage with security teams and shrug off potential hazards to user privacy. In these situations, vulnerability researchers are put in a difficult position: stay silent despite knowing users are at risk, or publicly disclose the vulnerability in an attempt to force the company into action. In the latter scenario, researchers may themselves put users in harm’s way by informing attackers of a potential path to exploitability.

ZK proofs of exploitability will radically shift how vulnerabilities are disclosed, allowing companies to precisely define bug bounty scope and researchers to unambiguously demonstrate they possess valid exploits, all without risking public disclosure.

Designing ZK proofs

In ZK proofs, a prover convinces a verifier that they possess a piece of information without revealing the information itself. For example, Alice might want to convince Bob that she knows the SHA256 preimage, X, of some value, Y, without actually telling Bob what X is. (Maybe X is Alice’s password). Perhaps the most well-known industrial application of ZK proofs is found in privacy-preserving blockchains like Zcash, where users want to submit transactions without revealing their identity, the recipient’s identity, or the amount sent. To do this, they submit a ZK proof showing that the transaction follows the blockchain’s rules and that the sender has sufficient funds. (Check out Matt Green’s blog post for a good introduction to ZK proofs with examples.)

Now you know why ZK proofs are useful, but how are these algorithms developed, and what tradeoffs need to be evaluated? There are three metrics to consider for developing an efficient system: prover time, verifier time, and bandwidth, which is the amount of data each party must send to the other throughout the protocol. Some ZK proofs don’t require interaction between the prover and verifier, in which case the bandwidth is just the size of the proof.

And now for the hard part, and the main barrier that has prevented ZK proofs from being used in practice. Many classical ZK protocols require that the underlying statement be first represented as a Boolean or arithmetic circuit with no loops (i.e., a combinatorial circuit). For Boolean circuits, we can use AND, NOT, and XOR gates, whereas arithmetic circuits use ADD and MULT gates. As you might imagine, it can be challenging to translate a statement you wish to prove into such a circuit, and it’s particularly challenging if that problem doesn’t have a clean mathematical formulation. For example, any program with looping behavior must be unrolled prior to circuit generation, which is often impossible when the program contains data-dependent loops.


Examples of Boolean and arithmetic circuits

Furthermore, circuit size has an impact on the efficiency of ZK protocols. Prover time usually has at least a linear relationship with circuit size (often with large constant overhead per gate). Therefore, ZK proofs in vulnerability disclosure require the underlying exploit to be captured by a reasonably sized circuit.

Proving Exploitability

Since ZK proofs generally accept statements written as Boolean circuits, the challenge is to prove the existence of an exploit by representing it as a Boolean circuit that returns “true” only if the exploit succeeds.

We want a circuit that accepts if the prover has some input to a program that leads to an exploit, like a buffer overflow that leads to the attacker gaining control of program execution. Since most binary exploits are both binary- and processor-specific, our circuit will have to accurately model whatever architecture the program was compiled to. Ultimately, we need a circuit that accepts when successful runs of the program occur and when an exploit is triggered during execution.

Taking a naive approach, we would develop a circuit that represents “one step” of whatever processor we want to model. Then, we’d initialize memory to contain the program we want to execute, set the program counter to wherever we want program execution to start, and have the prover run the program on their malicious input—i.e., just repeat the processor circuit until the program finishes, and check whether an exploit condition was met at each step. This could mean checking whether the program counter was set to a known “bad” value, or a privileged memory address was written to. An important caveat about this strategy: The entire processor circuit will need to run at each step (even though only one instruction is being actually executed), because singling out one piece of functionality would leak information about the trace.

Unfortunately, this approach will produce unreasonably large circuits, since each step of program execution will require a circuit that models both the core processor logic and the entirety of RAM. Even if we restrict ourselves to machines with 50 MB of RAM, producing a ZK statement about an exploit whose trace uses 100 instructions will cause the circuit to be at least 5 GB. This approach is simply too inefficient to work for meaningful programs. The key problem is that circuit size scales linearly with both trace length and RAM size. To get around this, we follow the approach of SNARKs for C, which divides the program execution proof into two pieces, one for core logic and the other for memory correctness.

To prove logic validity, the processor circuit must be applied to every sequential pair of instructions in the program trace. The circuit can verify whether one register state can legitimately follow the other. If every pair of states is valid, then the circuit accepts. Note, however, that memory operations are assumed to be correct. If the transition function circuit were to include a memory checker, it would incur an overhead proportional to the size of the RAM being used.

Trace Proof (1)

Checking processor execution validity without memory

Memory can be validated by having the prover also input a memory-sorted execution trace. This trace places one trace entry before the other if the first accesses a lower-numbered memory address than the second (with timestamps breaking ties). This trace lets us do a linear sweep of memory-sorted instructions and ensure consistent memory access. This approach avoids creating a circuit whose size is proportional to the amount of RAM being used. Rather, this circuit is linear in the trace size and only performs basic equality checks instead of explicitly writing down the entirety of RAM at each step.

Memory Proof (1)

Checking a memory sorted trace

The final issue we need to address is that nothing stops the prover from using a memory-sorted trace that doesn’t correspond to the original and create a bogus proof. To fix this, we have to add a “permutation checker” circuit that verifies we’ve actually sorted the program trace by memory location. More discussion on this can be found in the SNARKs for C paper.

Modeling x86

Now that we know how to prove exploits in ZK, we need to model relevant processor architectures as Boolean circuits. Prior work has done this for a RISC architecture called TinyRAM, which was designed to run efficiently in a ZK context. Unfortunately, TinyRAM is not used in commercial applications and is therefore not realistic for providing ZK proofs of exploitability in real-world programs, since many exploits rely on architecture-specific behavior.

We will begin our development of ZK proofs of exploitability by modeling a relatively simple microprocessor that is in widespread use: the MSP430, a simple chip found in a variety of embedded systems. As an added bonus, the MSP430 is also the system the Microcorruption CTF runs on. Our first major goal is to produce ZK proofs for each Microcorruption challenge. With this “feasibility demonstration” complete, we will set our sights on x86.

Moving from a simple RISC architecture to an infamously complex CISC machine comes with many complications. Circuit models of RISC processors clock in between 1–10k gates per cycle. On the other hand, if our x86 processor turned out to contain somewhere on the order of 100k gates, a ZK proof for an exploit that takes 10,000 instructions to complete would produce a proof of size 48 gigabytes. Since x86 is orders of magnitude more complex than MSP430, naively implementing its functionality as a Boolean circuit would be impractical, even after separating the proof of logic and memory correctness.

Our solution is to take advantage of the somewhat obvious fact that no program uses all of x86. It may be theoretically possible for a program to use all 3,000 or so instructions supported by x86, but in reality, most only use a few hundred. We will use techniques from program analysis to determine the minimal subset of x86 needed by a given binary and dynamically generate a processor model capable of verifying its proper execution.

Of course, there are some x86 instructions that we cannot support, since some x86 instructions implement data-dependent loops. For example, repz repeats the subsequent instruction until rcx is 0. The actual behavior of such an instruction cannot be determined until runtime, so we cannot support it in our processor circuit, which must be a combinatorial circuit. To handle such instructions, we will produce a static binary translator from normal x86 to our program-specific x86 subset. This way, we can handle the most complex x86 instructions without hard-coding them into our processor circuit.

A new bug disclosure paradigm

We are very excited to start this work with Johns Hopkins University and our colleagues participating in the DARPA SIEVE Program. We want to produce tools that radically shift how vulnerabilities are disclosed, so companies can precisely specify the scope of their bug bounties and vulnerability researchers can securely submit proofs that unambiguously demonstrate they possess a valid exploit. We also anticipate that the ZK disclosure of vulnerabilities can serve as a consumer protection mechanism. Researchers can warn users about the potential dangers of a given device without making that vulnerability publicly available, which puts pressure on companies to fix issues they may not have been inclined to otherwise.

More broadly, we want to transition ZK proofs from academia to industry, making them more accessible and practical for today’s software. If you have a specific use for this technology that we haven’t mentioned here, we’d like to hear from you. We’ve built up expertise navigating the complex ecosystem of ZK proof schemes and circuit compilers, and can help!

Bug Hunting with Crytic

Crytic, our Github app for discovering smart contract flaws, is kind of a big deal: It detects security issues without human intervention, providing continuous assurance while you work and securing your codebase before deployment.

Crytic finds many bugs no other tools can detect, including some that are not widely known. Right now, Crytic has 90+ detectors, and we’re continuously adding new checks and improving existing ones. It runs these bug and optimization detectors on every commit, and evaluates custom security properties that you add yourself too!

Today, we’re sharing twelve issues in major projects that were found solely by Crytic, including some of high severity.

Here are the issues we discovered. Read on for where we found them:

  1. Unused return value can allow free token minting
  2. registerVerificationKey always returns empty bytes
  3. MerkleTree.treeHeight and MerkleTree.zero can be constant
  4. Modifiers can return the default value
  5. Dangerous strict equality allows the contract to be trapped
  6. ABI encodePacked collision
  7. Missing inheritance is error-prone
  8. Msg.value is used two times in fundWithAward
  9. Reentrancy might lead to theft of tokens
  10. [Pending acknowledgement]
  11. [Pending acknowledgement]
  12. [Pending acknowledgement]

Ernst & Young Nightfall

Crytic found three bugs in E&Y’s Nightfall project, including one critical vulnerability that could allow anyone to mint free tokens.

Issue 1: Unused return value can allow minting free tokens


FTokenShield.mint does not check the return value of transferFrom. If FTokenShield is used with a token that does not revert in case of incorrect transfers, and only returns false (e.g., BAT), anyone can mint free commitments—and an attacker can mint tokens for free.

A similar issue with less impact occurs in FTokenShield.burn: here fToken.transfer is not checked.


Check the return value of transferFrom and transfer.

Crytic report

Issue 2: registerVerificationKey always returns empty bytes


FTokenShield.registerVerificationKey and NFTokenShield.registerVerificationKey return an empty bytes32. It is unclear what the correct returned value should be. This might lead to unexpected behavior for third parties and contracts.


Consider either returning a value, or removing the return value from the signature.

Crytic report

Issue 3: MerkleTree.treeHeight and MerkleTree.zero can be constant


treeHeight and zero can be declared constant in MerkleTree.sol to allow the compiler to optimize this code.


State variables that never change can be declared constant to save gas.

Crytic report


Crytic found one unusual issue in DeFiStrategies: The lack of placeholder execution in a modifier leads the caller function to return the default value. Additionally, Crytic found an issue related to strict equality on the return of a balanceOf call.

Issue 4: Modifiers can return the default value


The SuperSaverZap.onlyInEmergency() and SuperSaverZap.stopInEmergency() modifiers do not revert in case of invalid access. If a modifier does not execute or revert, the execution of the function will return the default value, which can be misleading for the caller.


Replace the if() condition by a require in both modifiers.

Crytic report

Issue 5: Dangerous strict equality allows the contract to be trapped


ERC20toUniPoolZapV1_General.addLiquidity has strict equality on the _UniSwapExchangeContractAddress balance. This behavior might allow an attacker to trap the contract by sending tokens to _UniSwapExchangeContractAddress.


Change == to <= in the comparison.

Crytic report


Crytic found another issue that is not well known in DOSNetwork: If abi.encodedPacked is called with multiple dynamic arguments, it can return the same value with different arguments.

Issue 6: ABI encodePacked Collision


DOSProxy uses the encodePacked Solidity function with two consecutive strings (dataSource and selector): eth-contracts/contracts/DOSProxy.sol.

This schema is vulnerable to a collision, where two calls with a different dataSource and selector can result in the same queryId (see the Solidity documentation for more information).


Do not use more than one dynamic type in encodePacked, and consider hashing both dataSource and selector with keccak256 first.

Crytic Report


Crytic found an architectural issue in the Baseline Protocol, among others: A contract implementing an interface did not inherit from it.

Issue 7: Missing inheritance is error-prone


Shield is an implementation of ERC1820ImplementerInterface, but it does not inherit from the interface. This behavior is error-prone and might prevent the implementation or the interface from updating correctly.


Inherit Shield from ERC1820ImplementerInterface.

Crytic report


Crytic found another unusual issue in EthKidsthis.balance includes the amount of the current transaction (msg.value), which might lead to incorrect value computation.

Issue 8: Msg.value is used two times in fundWithAward


The use of this.balance in fundWithAward does not account for the value already added by msg.value. As a result, the price computation is incorrect.

fundWithAward computes the token amount by calling calculateReward with msg.value:

function fundWithAward(address payable _donor) public payable onlyWhitelisted {
   uint256 _tokenAmount = calculateReward(msg.value, _donor);

calculateReward calls calculatePurchaseReturn, where _reserveBalance is this.balance and _depositAmount is msg.value:

  return bondingCurveFormula.calculatePurchaseReturn(_tokenSupply, _tokenBalance, address(this).balance, _ethAmount);

In calculatePurchaseReturnn, baseN is then computed by adding _depositAmount (msg.value) to _reserveAmount (this.balance):

uint256 baseN = _depositAmount.add(_reserveBalance);

msg.value is already present in this.balance. For example, if this.balance is 10 ether before the transaction, and msg.value is 1 eth, this.balance will be 11 ether during the transaction). As a result, msg.value is used two times, and calculatePurchaseReturn is incorrectly computed.


Change the price computation so that _reserveBalance does not include the amount sent in the transaction.

Crytic report


Finally, Crytic found a well-known issue in HQ20: reentrancy. This reentrancy is interesting as it occurs if the contract is used with a token with callback capabilities (such as ERC777). This is similar to the recent uniswap and lendf.me hacks.

Issue 9: Reentrancy might lead to theft of tokens


Classifieds calls transferFrom on external tokens without following the check-effects-interaction pattern. This leads to reentrancy that can be exploited by an attacker if the destination token has a callback mechanism (e.g., an ERC777 token).

There are two methods with reentrancy issues:


Follow the check-after-effect pattern.

Crytic report

Start using Crytic today!

Crytic can save your codebase from critical flaws and help you design safer code. What’s not to like?

Sign up for Crytic today. Got questions? Join our Slack channel (#crytic) or follow @CryticCi on Twitter.

Announcing the 1st International Workshop on Smart Contract Analysis

At Trail of Bits we do more than just security audits: We also push the boundaries of research in vulnerability detection tools, regularly present our work in academic conferences, and review interesting papers from other researchers (see our recent Real World Crypto and Financial Crypto recaps).

In this spirit, we and Northern Arizona University are pleased to co-organize the 1st International Workshop on Smart Contract Analysis (WoSCA 2020). Co-located with ISSTA 2020, our workshop will bring together researchers from all over the world to discuss static and dynamic approaches for analyzing smart contracts, static and dynamic. It covers, but is not limited to:

  • Analysis-based vulnerability discovery (e.g. heuristics-based static analysis, fuzzing)
  • Sound analysis (e.g. model checking, temporal logic)
  • Code optimization (e.g. code-size reduction, gas-cost estimation)
  • Code understanding (e.g. decompilation, reverse engineering)
  • Code monitoring (e.g. debugging, fault detection)
  • Intermediate representation (e.g. design, specification)

WoSCA 2020 also actively promotes open and reproducible research. We especially encourage you to submit papers that show how to improve existing tools or propose new ones!

Submit your paper (up to 8 pages) by Friday, May 22, 2020 (AoE).

And don’t forget: We’re still accepting submissions for the 10k Crytic Research Prize, which honors published academic papers built around or on top of our blockchain tools. Get involved!

Revisiting 2000 cuts using Binary Ninja’s new decompiler

It’s been four years since my blog post “2000 cuts with Binary Ninja.” Back then, Binary Ninja was in a private beta and the blog post response surprised its developers at Vector35. Over the past few years I’ve largely preferred to use IDA and HexRays for reversing, and then use Binary Ninja for any scripting. My main reason for sticking with HexRays? Well, it’s an interactive decompiler, and Binary Ninja didn’t have a decompiler…until today!

Today, Vector35 released their decompiler to their development branch, so I thought it’d be fun to revisit the 2000 cuts challenges using the new decompiler APIs.

Enter High Level IL

The decompiler is built on yet another IL, the High Level IL. High Level IL (HLIL) further abstracts the existing ILs: Low Level IL, Medium Level IL, and five others largely used for scripts. HLIL has aggressive dead code elimination, constant folding, switch recovery, and all the other things you’d expect from a decompiler, with one exception: Binary Ninja’s decompiler doesn’t target C. Instead, they’re focusing on readability, and I think that’s a good thing, because C is full of many idiosyncrasies and implicit operations/conversions, which makes it very difficult to understand.

Using one of our 2000 cuts challenges, let’s compare Binary Ninja’s decompiler to its IL abstractions.

First, the original disassembly:

The ASM disassembly has 43 instructions, of which three are arithmetic, 27 memory operations (loads, stores), four transfers, one comparison, and eight control flow instructions. Of these instructions, we care mainly about the control flow instructions and a small slice of memory operations.

Next, Low Level IL (LLIL):

LLIL mode doesn’t remove any instructions; it simply provides us a consistent interface to write scripts against, regardless of architecture being disassembled.

With Medium Level IL (MLIL), things start to get better:

In MLIL, stack variables are identified, dead stores are eliminated, constants are propagated, and calls have parameters. And we’re down to 17 instructions (39% of the original). Since MLIL understands the stack frame, all the arithmetic operations are removed and all the “push” and “pop” instructions are eliminated.

Now, in the decompiler, we’re down to only six instructions (or eight, if you count the variable declarations):

Also available in linear view:


HLIL Linear View

Using the new decompiler API to solve 2000 cuts

For the original challenge, we had to extract hard-coded stack canaries out of hundreds of nearly identical executables. I was able to do this with very little difficulty using the LLIL API, but I had to trace some values around and it was a bit unergonomic.

Let’s try it again, but with the HLIL API1:

Running the script produces the desired result:

We quickly process 1000 cuts


The HLIL solution is a bit more concise than our original, and easier to write. Overall, I’m enjoying the Binary Ninja’s new decompiler and I’m pretty excited to throw it at architectures not supported by other decompilers, like MIPS, 68k, and 6502. Hopefully, this is the decade of the decompiler wars!

If you’re interested in learning more about Binary Ninja, check out our Automated Reverse Engineering with Binary Ninja training.

  1. For help writing Binary Ninja plugins that interact with the ILs, check out my bnil-graph plugin, which was recently updated to support HLIL.

Announcing our first virtual Empire Hacking

At Trail of Bits, we’ve all been working remotely due to COVID-19. But the next Empire Hacking event will go on, via video conference!

  • When: April 14th @ 6PM
  • How: RSVP via this Google Form or on Meetup. We’ll email you an invitation early next week.

Come talk shop with us!

Every two months, Empire Hacking is hosted by companies that share our passion for investigating the latest in security engineering. We bring together interesting speakers and people in the field, share new information, make connections, and enjoy continuing our conversations at a nearby bar afterwards. (Bring your own quarantini this time.)

Don’t miss our April lineup

Enarx-Secured, Attested Execution on Any Cloud

Lily Sturmann and Mark Bestavros, security engineers at Red Hat in Boston, will tell us the latest about their work on the open-source Enarx project, which is currently underway on AMD’s SEV and Intel’s SGX hardware. Enarx makes it simple to deploy confidential workloads to a variety of TEEs in the public cloud by handling deployment and attestation. It uses WebAssembly to offer developers a wide range of compatible language choices for workloads, eliminating the need to rewrite the application for a particular TEE’s platform or SDK.

Towards Automated Vulnerability Patching

If you know Trail of Bits, you know we find a lot of bugs, and we think you’ll enjoy this peek at what happens after bugs are found. Carson Harmon will give a brief high-level overview of the challenges associated with vulnerability patching, and our progress in creating tools to assist humans with the process. He’s been working on DARPA CHESS, one of our government-sponsored projects that focuses on automatically finding and fixing bugs in C/C++ programs.

We look forward to seeing you (virtually) on April 14th at 6PM to continue the conversation.

An Echidna for all Seasons

TL;DR: We have improved Echidna with tons of new features and enhancements since it was released—and there’s more to come.

Two years ago, we open-sourced Echidna, our property-based smart contract fuzzer. Echidna is one of the tools we use most in smart contract assessments. According to our records, Echidna was used in about 35% of our smart contract audits during the past two years. These include several high-profile audits such as MakerDAO, 0x, and Balancer. Since the first release of Echidna, we have been adding new features as well as fixing bugs. Here’s a quick look at what we’ve done.

New features

We expanded the capabilities of Echidna with a large set of exciting new features. Some of the most important ones are:

Support for several compilation frameworks using crytic-compile: Integration with crytic-compile allowed Echidna to test complex Truffle projects, and even smart contracts in other languages, such as Vyper, right out of the box. It is completely transparent for the user (if you are an Echidna user, you are already using it!) and it was one of the most important features we implemented in Echidna last year.

Assertion testing: Solidity’s assert can be used as an alternative to explicit Echidna properties, especially if the conditions you’re checking are directly related to the correct use of some complex code deep inside a function. Assertion testing also lets you check for implicit asserts inserted by the compiler, such as out-of-bounds array accesses without an explicit property. Add checkAsserts: true in your Echidna configuration file and it will take care of the rest.

An assertion failure is discovered in Vera’s MakerDAO example

Restrict the functions to call during a fuzzing campaign: Not all functions in a smart contract are created equal. Some of them are not useful during property-based testing and will only slow down the campaign. That’s why Echidna can either blacklist or whitelist functions to call during a fuzzing campaign. Here’s an Echidna configuration that avoids “f1” and “f2” methods during a fuzzing campaign:

filterBlacklist: true # or use false for whitelisting
filterFunctions: ["f1", "f2"]

Save and load the corpus collected during a fuzzing campaign: If coverage support is enabled, Echidna can load and save the complete corpus collected in JSON. If a corpus is available at the beginning of a fuzzing campaign, Echidna will use it immediately. This means that Echidna will not start from scratch, which is particularly useful during CI tests to speed up the verification of complex properties. Add coverage: true and corpusDir: "corpus" to your Echidna configuration and create a “corpus” directory to save the inputs generated by Echidna.

Pretty-printed example of a transaction from a corpus.

Detect transactions with high-gas consumption: Excessive gas usage can be a pain for developers and users of smart contracts. There are few tools available for detecting transactions with large gas consumption, especially if detecting the transaction requires reaching unusual states of the contract via other transactions. Recently Echidna added support to detect this kind of issue. Use estimateGas: true in your Echidna configuration to report high-gas transactions to your console.

Discovery of a transaction consuming a large amount of gas

Extended testing of complex contracts: Echidna also improved the testing of complex contracts with two cool features. First, it allows initializing a fuzzing campaign with arbitrary transactions using Etheno. Second, it can test more than one contract at the same time, calling any public or external function of any tested contract. Use multi-abi: true in your Echidna configuration to test more than one contract at the same time.

Keeping up to date with the latest research

We are following the latest developments in smart contract fuzzing papers to make sure Echidna is up to date. Our researchers compare open-source fuzzers to Echidna, and integrate any new approach that proves to be effective for finding faults or generating more interesting inputs. In fact, from time to time, we test examples presented in research papers to make sure Echidna can solve them very efficiently! We also regularly attend conferences to discuss novel fuzzing techniques, and even financially support new research papers that improve our tools.

Echidna solves the example presented in Harvey’s paper

Looking forward

And we’re not taking a break! In fact, we have a pipeline of improvements and new features coming to Echidna in the near future, including enhanced coverage feedback, array generation and corpus mutations, and Slither integration. We are also excited to share that we have added Echidna support to crytic.io, our continuous assurance platform for smart contracts.

Echidna integration for automatic assertion checking in crytic.io

In summary

In two years, Echidna has evolved from an experimental tool into an essential resource for fuzzing smart contracts and identifying correctness/security issues. We continue to push the limits of what is possible by fuzzing smart contracts, and keep our open-source tools updated for community use. Learn more about testing your smart contracts with Echidna in our Building Secure Contracts training.

Do you have smart contracts to test with Echidna? Are you interested in reviewing your Echidna scripts or training on how to use it effectively? Drop us a line! Trail of Bits has years of experience in performing smart contract security assessments, addressing everything from minimalistic tokens to complex staking and voting platforms.

Announcing the Zeek Agent

(This posting is cross-posted between the Zeek blog and the Trail of Bits blog).

The Zeek Network Security Monitor provides a powerful open-source platform for network traffic analysis. However, from its network vantage point, Zeek lacks access to host-level semantics, such as the process and user accounts that are responsible for any connections observed. The new Zeek Agent fills this gap by interfacing Zeek directly with your endpoints, providing semantic context that’s highly valuable for making security decisions. The agent collects endpoint data through custom probes and, optionally, by interfacing to osquery and making most of its tables available to Zeek.

We are releasing the Zeek Agent as open-source code under the liberal BSD license. Head over to the releases page and try it now with your macOS and Linux endpoints; Windows support is coming soon! Please share your ideas, requests and other feedback with us by filing an issue on GitHub or joining the #zeek-agent channel on the new Zeek Slack.


What’s new here and why it’s useful

Traditionally, network security monitors only receive network traffic passively intercepted between hosts (endpoints). While that vantage point is very powerful—the network does not lie!—it does not provide the complete picture, and it can be challenging to understand the broader context of who is doing what on the endpoints. This approach makes analyzing encrypted traffic particularly challenging: Since passive monitoring cannot assess the actual content of the communication, defenders often remain in the dark about its legitimacy.

The Zeek Agent closes this gap by adding an endpoint-level vantage point to host activity. Just like Zeek itself, the policy-neutral agent does not perform any detection. Instead, it collects a stream of host-side events (“new process,” “socket opened,” “user logged in”) and feeds those events into Zeek’s standard processing pipeline, where they become available to Zeek scripts just like traditional network-derived events. By representing both network and host activity inside the same event abstraction, this setup lets users deploy all of Zeek’s powerful machinery to cross-correlate the two vantage points. For example, Zeek could now tag network connections with the endpoint-side services that initiated them (e.g., sshd). The agent can also let Zeek create new logs that record endpoint information, as seen in this example:

Screen Shot 2020-03-20 at 12.29.04 AM

Zeek logs of network connections and listening ports, enriched with relevant process context from the endpoint (provided by the Zeek Agent)

A short history and background of the project

In 2018 at the University of Hamburg, Steffen Haas developed an initial prototype of the agent. Originally called zeek-osquery, this prototype was a powerful demonstration of the agent approach, but it had certain technical limitations that precluded production usage.

In 2019, Corelight hired Trail of Bits to update and improve Haas’ zeek-osquery software prototype. While the prototype was developed as a set of patches that implemented functionality directly within the osquery core, Trail of Bits suggested a different approach that would be more suitable for long-term development, and a better match for existing deployments. The new version began as a port of the existing code to an osquery extension which could be packaged and distributed independently. Eventually, this process evolved into a clean rewrite to produce an entirely new agent that can operate both in a standalone fashion and with osquery. The agent’s built-in data sources leverage the same underlying process-monitoring capabilities as osquery, but in a way more compatible with how Linux systems are configured for real-world use. Trail of Bits also designed the agent to easily support more custom data sources in the future.

How the Zeek Agent works

Like osquery, the agent provides system information in the form of a database, using the SQLite library. Table plugins publish the actual data, and are allocated and registered during startup. Once they export the necessary methods to report the schema and generate data, the internal framework will create the required SQLite table abstractions and attach them to the database.

Most data sources will inspect the system at query time and report their findings at that specific point in time. However, some tables may want to keep listening for system activity even when no query is being executed. This is commonly referred to as an evented table, which typically uses threads/callbacks to continuously record system events in the background. The process_events table works exactly like this, and allows Zeek scripts to look at past process executions.

Additional data sources can be imported from osquery, if it happens to be installed and running on the same system, thanks to the extensions socket. With this design, everything appears to come from a single unified database, allowing users to seamlessly join built-in and osquery tables together.

The tables can be accessed via scripts as soon as the agent connects to a Zeek server instance. Data can be requested either by running a single-shot SQL statement or as a scheduled query that runs automatically and reports data at specified intervals.

On the Zeek side, scripts fully control the data requested from the agent by defining corresponding SQL queries. Results stream into Zeek continuously, and transparently turn into standard Zeek events that handlers can hook into, just as if the events were derived from network traffic.

How to get started

The Zeek Agent documentation summarizes how to build and install the agent. On the Zeek side, there’s a new Zeek Agent framework you can install through Zeek’s package manager. See its documentation for more information on installation and usage. For an example of a Zeek script requesting information from the agent, see this script that turns process activity into a Zeek log on Linux.

What’s next for the Zeek Agent?

Right now, we welcome feedback on the Zeek Agent regarding usability, functionality, and deployment models. We’re curious to see what use-cases the Zeek community comes up with, and we encourage users to publish Zeek packages that leverage the agent’s capabilities. The best places to leave feedback are the agent’s GitHub issues, the #zeek-agent channel on the new Zeek Slack, and the Zeek mailing list.

The agent is an open-source project, so we also appreciate code contributions; just file GitHub pull requests. If you are interested in sponsoring specific work on the Zeek Agent, please contact Corelight.

We continue to extend the agent: We just completed an initial port to macOS, and we’re working on Windows support, as well. We will be extending the Zeek-side agent script framework, and we‘re also adding a multi-hop routing layer to Zeek’s underlying communication system, Broker, to facilitate deployment of the Zeek Agent across numerous endpoints.

About Trail of Bits Security Engineering Services

As your secure development partner, Trail of Bits has helped some of the world’s leading security software companies bring reliable products to market. Our engineering team’s goal is to write secure code and build tools that users can trust to protect their organizations and data. With our teams’ combined software development experience and research into system-level security, we regularly identify foundational gaps: missing capabilities, opportunities for improvement, and even potential vulnerabilities. We will review existing software architecture and provide recommendations or fixes, enhance feature sets or write new capabilities, and improve your security testing using the best available tools.

If your organization has security software plans but lacks the time or dedicated engineering resources to ensure the final product adheres to the best practices in secure coding, contact us. We would love to hear from you.

About Corelight

Corelight delivers powerful network traffic analysis (NTA) solutions that help organizations defend themselves more effectively by transforming network traffic into rich logs, extracted files, and security insights. Corelight Sensors are built on Zeek (formerly called “Bro”), the open-source network security monitoring framework that generates actionable, real-time data for thousands of security teams worldwide. Zeek has become the “gold standard’’ for incident response, threat hunting, and forensics in large enterprises and government agencies worldwide. Founded by the team behind Zeek, Corelight makes a family of virtual and physical network sensors that take the pain out of deploying open-source Zeek and expand its performance and capabilities. Corelight is based in San Francisco, California, and its global customers include Fortune 500 companies, large government agencies, and major research universities. For more information, visit https://www.corelight.com.

Financial Cryptography 2020 Recap

A few weeks ago, we went to the 24th Financial Cryptography (FC) conference and the Workshop on Trusted Smart Contracts (WTSC), where we presented our work on smart contract bug categorization (see our executive summary) and a poster on Echidna. Although FC is not a blockchain conference, it featured several blockchain-oriented presentations this year and in previous years. And despite issues stemming from world-traveling restrictions, the organizers pulled off an excellent conference for 2020.

Here are some of the conference papers we recommend checking out:


Security Analysis on dBFT Protocol of NEO

Qin Wang, Jiangshan Yu, Zhiniang Peng, Van Cuong Bui, Shiping Chen, Yong Ding, and Yang Xiang

In this review of the NEO blockchain’s consensus protocol, dBFT (a variant of the standard PBFT), the authors discovered two successful safety attacks which occurred mostly because dBFT skipped a specific message (COMMIT) for optimization reasons. We’ve reviewed similar consensus protocols at Trail of Bits, and we enjoyed learning about the attacks found here.

Breaking the Encryption Scheme of the Moscow Internet Voting System

Pierrick Gaudry and Alexander Golovnev

We’ve reviewed several on-chain election systems, so this system’s vulnerabilities were no surprise to us. In this study, the encryption of an on-chain voting system in a recent Moscow election used a variant of ElGamal called 3 ElGamal, which is a multi-level encryption version of ElGamal. It is not clear why the developers created this variant, since it does not increase security. They used 256-bit keys, which (as you might expect) are too small; However, the paper’s authors believe 256-bit keys were used because they match the size of EVM operands and allowed a simple on-chain implementation of the encryption. The issue was reported a few weeks before the election, so the developers rewrote most of the codebase and removed the on-chain encryption just before the election. The authors then found another issue that caused a leak of one bit of information—enough to identify a voter’s choice of candidate. Not surprisingly, this paper had significant press coverage (Coindesk, ZDnet, etc.).

LockDown: Balance Availability Attack Against Lightning Network Channels

Cristina Pérez-Solà, Alejandro Ranchal-Pedrosa, Jordi Herrera-Joancomartí, Guillermo Navarro-Arribas, and Joaquin Garcia-Alfaro

In this paper, the authors showed that it is possible to trigger a balance lockdown on the bitcoin lightning network. Essentially, an attacker can reach a dominant position over its target in the network such that it becomes the main gateway of the route payment. Interestingly enough, payment channels allow loops in their path, increasing the fee for the attacker.

Selfish Mining Re-examined

Kevin Alarcón Negy, Peter Rizun, and Emin Gün Sirer

At a high level, selfish mining occurs when a miner does not reveal that a block has been mined. Knowing the block has been mined, the selfish miner can work on the next one and thereby gain an edge over the competition. Selfish mining is a known concept in blockchain, but part of the community believes the reasoning is flawed and the attack is not profitable.

This paper introduces a variant in which a miner switches between selfish mining and standard mining, and shows how a miner would profit from such behavior. They looked at the difficulty adjustment algorithms, and found that some blockchains seem more vulnerable than others. Typically, Ethereum’s uncle reward—in which miners receive a small reward if competitive blocks are mined (i.e., when two miners find a different block at the same time)—seems to make Ethereum more vulnerable.

Program analysis

Marlowe: Implementing and Analysing Financial Contracts on Blockchain

Pablo Lamela Seijas, Alexander Nemish, David Smith, and Simon Thompson

Marlowe is a Haskel-based DSL meant to represent financial contracts on the Cardano blockchain. The DSL is not Turing-complete, but aims to provide all the features necessary for the most common financial contracts. It is a nice work in progress; check it out their web-based IDE.

Enforcing Determinism of Java Smart Contracts

Fausto Spoto

This work focuses on the Takamaka blockchain, which allows smart contracts to be written in Java and executed in a Java virtual machine. One of the main issues with Java is keeping deterministic execution, while some standard libraries are not deterministic (e.g., HashSet). This work-in-progress uses a whitelist approach of known deterministic libraries, and statically detects when a function call is dangerous; it then adds dynamic instrumentation and reverts the contract if non-deterministic behavior is detected.

Albert, an Intermediate Smart-Contract Language for the Tezos Blockchain

Bruno Bernardo, Raphaël Cauderlier, Basile Pesin, and Julien Tesson

Albert is an intermediate representation for the Tezos blockchain. Its compiler to Michelson, the language executed on Tezos, was written and verified in Coq. It is nice work in progress, and we were happy to see compiler verification applied to smart contract language.

A Formally Verified Static Analysis Framework for Compositional Contracts

Fritz Henglein, Christian Kjær Larsen, and Agata Murawska

This work presents an abstract interpretation framework based on the Contract Specification Language (CSL). The work is interesting, but unfortunately, CSL has not yet found much real-world usage.

Protocol design

Load Balancing in Sharded Blockchains

Naoya Okanami, Ryuya Nakamura, and Takashi Nishide

This paper focused on the sharding repartition for Eth 2.0. With Eth 2.0, smart contracts will be split between shards, and then one must determine which contract is in what shard. It’s a hot topic, with many different approaches. For example, Eth 2.0 might end with a “Yank” opcode, allowing a contract to switch between shards. This work proposes a load-balancing approach, where off-chain competitors submit different repartitions and earn a reward if their solution is picked.

Fairness and Efficiency in DAG-Based Cryptocurrencies

Georgios Birmpas, Elias Koutsoupias, Philip Lazos, and Francisco J. Marmolejo-Cossío

DAG-based public ledgers are an alternative to blockchain. Instead of storing the history of the chain in a linear data structure, some teams try to use a DAG (directed acyclic graph). DAG-based ledgers are supposed to scale significantly better than blockchain, but they create a difficult architecture to synchronize. This paper proposed a scenario in which there is no malicious miner, and showed that even in this situation, the synchronization is difficult and depends heavily on miner connectivity.

Decentralized Privacy-Preserving Netting Protocol on Blockchain for Payment Systems

Shengjiao Cao, Yuan Yuan, Angelo De Caro, Karthik Nandakumar, Kaoutar Elkhiyaoui, and Yanyan Hu

Done in collaboration with IBM, this work used zk-proof to create a decentralized netting and allow banks to settle their balances. See the code.

MicroCash: Practical Concurrent Processing of Micropayments

Ghada Almashaqbeh, Allison Bishop, and Justin Cappos

In this paper, the authors created a micro-payment solution that handles parallel payments. Most existing micro-payment solutions require sequential payment, which limits their usage. The author extended the existing probabilistic micropayment schema. One limitation is that the system requires a relatively stable set of merchants, but it is likely to match most real-world situations.

Ride the Lightning: The Game Theory of Payment Channels

Zeta Avarikioti, Lioba Heimbach, Yuyi Wang, and Roger Wattenhofer

Here, the authors use a game theory approach for economic modeling of payment channels. They used graph-based metrics (betweenness and closeness centrality) and aimed to minimize the user’s cost (channels’ creation cost) while maximizing fees. It is an interesting approach. Some assumptions are not realistic (e.g., it assumes that all the nodes are static), but their approach shows that there are improvements to be made in the nodes’ strategies for their payment channel position.

How to Profit From Payment Channels

Oğuzhan Ersoy, Stefanie Roos, and Zekeriya Erkin

When the authors looked at the fee chosen by the nodes in a payment channel, most of the nodes seemed to use the default value. This work formalizes the optimization problem of having the optimal fee for a node, and shows that the problem is NP-hard. It then proposes a greedy algorithm to find an approximation to the optimal solution. Here they assume that other nodes keep a fee constant, which is realistic for now, but might change if nodes start using more efficient fee strategies.

High-level studies

Surviving the Cryptojungle: Perception and Management of Risk Among North American Cryptocurrency (Non)Users

Artemij Voskobojnikov, Borke Obada-Obieh, Yue Huang, and Konstantin Beznosov

This is a user study on the perception and management of the risks associated with cryptocurrency. It is an interesting work focusing on cryptocurrency in general, not just bitcoin. As expected, the authors found that many users struggle with the user-interface of wallet and blockchain applications, and several users studied are afraid of using cryptocurrency and are waiting for more regulations.

Characterizing Types of Smart Contracts in the Ethereum Landscape

Monika di Angelo and Gernot Salzer

This study focuses on classifying activity on the Ethereum mainet. It confirms some known results: A lot of code is duplicated and/or unused. The paper also shows that GasTokens are responsible for a significant percentage of transactions. Such a classification is needed to better understand the different trends and usages of blockchain.

Smart Contract Development From the Perspective of Developers: Topics and Issues Discussed on Social Media.

Afiya Ayman, Shanto Roy, Amin Alipour, and Aron Laszka

This paper took an interesting approach to security questions and tool citation by showing which tools are cited most often in Stack Exchange and Medium. It would be interesting to apply this approach to other media (Reddit, Twitter), and look at the software quality of the tools. For example, Oyente is frequently cited, but the tool has not been updated since 2018 and is no longer usable.

Systematization of knowledge

SoK: A Classification Framework for Stablecoin Designs

Amani Moin, Kevin Sekniqi, and Emin Gun Sirer

This work classifies the different stablecoins and will be a useful reference. We were interested in this work since we reviewed many of the stablecoins cited.

SoK: Layer-Two Blockchain Protocols

Lewis Gudgeon, Pedro Moreno-Sanchez, Stefanie Roos, Patrick McCorry, and Arthur Gervai

The paper summarizes different layer-two solutions, and will be a useful reference for anyone working on this topic.

Secure computation

Communication-Efficient (Client-Aided) Secure Two-Party Protocols and Its Application

Satsuya Ohata and Koji Nuida

This paper focused on MPCs based on shared-secret (SS), which are faster than traditional garbled circuits. The main issue with most SS-based MPCs is the number of communication rounds required, which creates significant network latency. This makes MPCs impractical to deploy on a WAN setup, which seems to be an anti-goal for MPC. The authors focus on reducing the number of communication rounds so SS-based MPC can be deployed on WAN.

Insured MPC: Efficient Secure Computation with Financial Penalties

Carsten Baum, Bernardo David, and Rafael Dowsley

In this presentation on the security properties of MPC, the authors explain that traditional works focus mostly on the correctness and privacy of MPC, but some properties are missing. The security of an MPC also relies on fairness (if an adversary gets output, everybody does), identifiable abort (if an adversary aborts, every party knows who caused it), and public verification (any third party can verify that the output was correctly computed). As a result, the authors propose the construction of a publicly verifiable homomorphic commitment scheme with composability guarantees.

Secure Computation of the kth-Ranked Element in a Star Network

Anselme Tueno, Florian Kerschbaum, Stefan Katzenbeisser, Yordan Boev, and Mubashir Qureshi

Here the authors propose a protocol to find the kth-ranked element when multiple parties hold private integers (e.g., comparing employee salaries without revealing the salaries). The main idea is to use a server in a secure multiparty computation (SMC); the server is meant to help the protocol without having access to private information.


Zether: Towards Privacy in a Smart Contract World

Benedikt Bünz, Shashank Agrawal2, Mahdi Zamani2, and Dan Boneh

Zether leverages zk-proofs to allow private fund transfers. It is a hot topic; we previously worked on Aztec, which proposes a similar solution. While the bulletproof library is open-source, the smart contract seems to be closed-source.

BLAZE: Practical Lattice-Based Blind Signatures for Privacy-Preserving Applications

Nabil Alkeilani Alkadri, Rachid El Bansarkhani, and Johannes Buchmann

This paper proposes a post-quantum blind signature schema. Blaze aims to improve two current limitations of the existing schema, i.e., they are either too slow or their signatures are too large.

Submit your research to our Crytic Research Prize!

FC is one of the peer-reviewed conferences recommended in our Crytic $10k cash prize. If you are working on program analysis for smart contracts, try any of our open-source tools (including Slither, Echidna, Manticore) and submit your work for our Crytic prize! We are happy to provide technical support to anyone using our tools for academic research—just contact us.

Real-time file monitoring on Windows with osquery

TL;DR: Trail of Bits has developed ntfs_journal_events, a new event-based osquery table for Windows that enables real-time file change monitoring. You can use this table today to performantly monitor changes to specific files, directories, and entire patterns on your Windows endpoints. Read the schema documentation here!

The results of a query on ntfs_journal_events

File monitoring for fleet security and management purposes

File event monitoring and auditing are vital primitives for endpoint security and management:

  • Many malicious activities are reliably sentineled or forecast by well-known and easy to identify patterns of filesystem activity: rewriting of system libraries, dropping of payloads into fixed locations, and (attempted) removal of defensive programs all indicate potential compromise
  • Non-malicious integrity violations can also be detected through file monitoring: employees jailbreaking their company devices or otherwise circumventing security policies
  • Software deployment, updating, and automated configuration across large fleets: “Does every host have Software X installed and updated to version Y?”
  • Automated troubleshooting and remediation of non-security problems: incorrect permissions on shared files, bad network configurations, disk (over)utilization

A brief survey of file monitoring on Windows

Methods for file monitoring on Windows typically fall into one of three approaches:

We’ll cover the technical details of each of these approaches, as well as their advantages and disadvantages (both general and pertaining to osquery) below.

Win32 APIs

The Windows API provides a collection of (mostly) filesystem-agnostic functions for polling for events on a registered directory:

These routines come with several gotchas:

FindFirstChangeNotification does not monitor the specified directory itself, only its entries. Consequently, the “correct” way to monitor both a directory and its entries is to invoke the function twice: once for the directory itself, and again for its parent (or drive root). This, in turn, requires additional filtering if the only entry of interest in the parent is the directory itself.

These routines provide the filtering and synchronization for retrieving filesystem events, but do not expose the events themselves or their associated metadata. The actual events must be retrieved through ReadDirectoryChangesW, which takes an open handle to the watched directory and many of the same parameters as the polling functions (since it can be used entirely independently of them). Users must also finagle with the bizarre world of OVERLAPPED in order to use ReadDirectoryChangesW safely in an asynchronous context.

ReadDirectoryChangesW can be difficult to use with the Recycling Bin and other pseudo-directory concepts on Windows. This SO post suggests that the final moved name can be resolved with GetFinalPathNameByHandle. This GitHub issue suggests that the function’s behavior is also inconsistent between Windows versions.

Last but not least, ReadDirectoryChangesW uses a fixed-size buffer for each directory handle internally and will flush all change records before they get handled if it cannot keep up with the number of events. In other words, its internal buffer does not function as a ring, and cannot be trusted to degrade gradually or gracefully in the presence of lots of high I/O loads.

An older solution also exists: SHChangeNotifyRegister can be used to register a window as the recipient of file notifications from the shell (i.e., Explorer) via Windows messages. This approach also comes with numerous downsides: it requires the receiving application to maintain a window (even if it’s just a message-only window), uses some weird “item-list” view of filesystem paths, and is capped by the (limited) throughput of Windows message delivery.

All told, the performance and accuracy issues of these APIs make them poor candidates for osquery.

Filter drivers and minifilters

Like so many other engineering challenges in Windows environments, file monitoring has a nuclear option in the form of a kernel-mode APIs. Windows is kind enough to provide two general categories for this purpose: the legacy file system filter API and the more recent minifilter framework. We’ll cover the latter in this post, since it’s what Microsoft recommends.

Minifilters are kernel-mode drivers that directly interpose the I/O operations performed by Windows filesystems. Because they operate at the common filesystem interface layer, minifilters are (mostly) agnostic towards their underlying storage — they can (in theory) interpose any of the filesystem operations known by the NT kernel regardless of filesystem kind or underlying implementation. Minifilters are also composable, meaning that multiple filters can be registered against and interact with a filesystem without conflict.

Minifilters are implemented via the Filter Manager, which establishes a filter loading order based on a configured unique “altitude” (lower altitudes corresponding to earlier loads, and thus earlier access) and presence in a “load order group”, which corresponds to a unique range of altitudes. Load order groups are themselves loaded in ascending order with their members loaded in random order, meaning that having a lower altitude than another minifilter in the same group as you does not guarantee higher precedence. Microsoft provides some documentation for (public) load order groups and altitude ranges here; a list of publicly known altitudes is available here. You can even request one yourself!

While powerful and flexible and generally the right choice for introspecting the filesystem on Windows, minifilters are unsuitable for osquery’s file monitoring purposes:

  • For in-tree (i.e., non-extension) tables, osquery has a policy against system modifications. Installing a minifilter requires us to modify the system by loading a driver, and would require osquery to either ship with a driver or fetch one at install-time.
  • Because minifilters are full kernel-mode drivers, they come with undesirable security and stability risks.
  • The design of osquery makes certain assurances to its users: that it is a single-executable, user-mode agent, self-monitoring its performance overhead at runtime — a kernel-mode driver would violate that design.

Journal monitoring

A third option is available to us: the NTFS journal.

Like most (relatively) modern filesystems, NTFS is journaled: changes to the underlying storage are preceded by updates to a (usually circular) region that records metadata associated with the changes. Dan Luu’s “Files are fraught with peril” contains some good motivating examples of journaling in the form of an “undo log”.

Journaling provides a number of benefits:

  • Increased resilience against corruption: the full chain of userspace-to-kernel-to-hardware operations for an single I/O operation (e.g., unlinking a file) isn’t internally atomic, meaning that a crash can leave the filesystem in an indeterminate or corrupted state. Having journal records for the last pre-committed operations makes it more likely that the filesystem can be rolled back to a known good state.
  • Because the journal provides a reversible record of filesystem actions, interactions with the underlying storage hardware can be made more aggressive: the batch size for triggering a commit can be increased, increasing performance.
  • Since the journal is timely and small (relative to the filesystem), it can be used to avoid costly filesystem queries (e.g., stat) for metadata. This is especially pertinent on Windows, where metadata requests generally involve acquiring a full HANDLE.

NTFS’s journaling mechanism is actually split into two separate components: $LogFile is a write-ahead log that handles journaling for rollback purposes, while the change journal ($Extend\$UsnJrnl) records recent changes on the volume by kind (i.e., without the offset and size information needed for rollback).

Windows uses the latter for its File History feature, and it’s what we’ll use too.

Accessing the change journal

⚠ The samples below have been simplified for brevity’s sake. They don’t contain error handling and bounds checking, both of which are essential for safe and correct use. Read MSDN and/or the full source code in osquery before copying! ⚠

Fortunately for us, opening a handle to and reading from the NTFS change journal for a volume is a relatively painless affair with just a few steps.

  1. We obtain the handle for the volume that we want to monitor via a plain old CreateFile call:ntfs0
  2. We issue a DeviceIoControl[FSCTL_QUERY_USN_JOURNAL] on the handle to get the most recent Update Sequence Number (USN). USNs uniquely identify a batch records committed together; we’ll use our first to “anchor” our queries chronologically:ntfs1
  3. We issue another DeviceIoControl, this time with FSCTL_READ_USN_JOURNAL, to pull a raw buffer of records from the journal. We use a READ_USN_JOURNAL_DATA_V1 to tell the journal to only give us records starting at the USN we got in the last step:ntfs2

Mind the last two fields (2U and 3U) — they’ll be relevant later.

Interpreting the change record buffer

DeviceIoControl[FSCTL_READ_USN_JOURNAL] gives us a raw buffer of variable-length USN_RECORDs, prefixed by a single USN that we can use to issue a future request:


Then, in our process_usn_record:


Recall those last two fields from READ_USN_JOURNAL_DATA_V1 — they correspond to the range of USN_RECORD versions returned to us, inclusive. We explicitly exclude v4 records, since they’re only emitted as part of range tracking and don’t include any additional information we need. You can read more about them on their MSDN page.

MSDN is explicit about these casts being necessary: USN_RECORD is an alias for USN_RECORD_V2, and USN_RECORD_V3 is not guaranteed to have any common layout other than that defined in USN_RECORD_COMMON_HEADER.

Once that’s out of the way, however, the following fields are available in both:

  • Reason: A bitmask of flags indicating changes that have accumulated in the current record. See MSDN’s USN_RECORD_V2 or USN_RECORD_V3 for a list of reason constants.
  • FileReferenceNumber: A unique (usually 128-bit) ordinal referencing the underlying filesystem object. This is the same as the FRN that can be obtained by calling GetFileInformationByHandleEx with FileIdInfo as the information class. FRNs correspond roughly to the “inode” concept in UNIX-land, and have similar semantics (unique per filesystem, not system-wide).
  • ParentFileReferenceNumber: Another FRN, this one for the parent directory (or volume) of the file or directory that this record is for.
  • FileNameLength, FileNameOffset, FileName: The byte-length, offset, and pointer to the filename of the file or directory that this is for. Note that FileName is the base (i.e., unqualified) name — retrieving the fully qualified name requires us to resolve the name of the parent FRN by opening a handle to it (OpenFileById), calling GetFinalPathNameByHandle, and joining the two.

Boom: file events via the change journal. Observe that our approach has sidestepped many of the common performance and overhead problems in file monitoring: we operate completely asynchronously and without blocking the filesystem whatsoever. This alone is a substantial improvement over the minifilter model, which imposes overhead on every I/O operation.


Like the other techniques mentioned, the change journal approach to file monitoring is not without its disadvantages.

As the name of the table suggests, change journal monitoring only works on NTFS (and ReFS, which appears to be partially abandoned). It can’t be used to monitor changes on FAT or exFAT volumes, as these lack journaling entirely. It also won’t work on SMB shares, although it will work on cluster-shared volumes of the appropriate underlying format.

Handling of rename operations is also slightly annoying: the change journal records one event for the “old” file being renamed and another for the “new” file being created, meaning that we have to pair the two into a single event for coherent presentation. This isn’t hard (the events reference each other and have distinct masks), but it’s an extra step.

The change journal documentation is also conspicuously absent of information about the possibility of dropped records: the need for a start USN and the returning of a follow-up USN in the raw buffer imply that subsequent queries are expected to succeed, but no official details about the size of wraparound behavior of the change journal are provided. This blog post indicates that the default size is 1MB, which is probably sufficient for most workloads. It’s also changeable via fsutil.

Potentially more important is this line in the MSDN documentation for the Reason bitmask:

The flags that identify reasons for changes that have accumulated in this file or directory journal record since the file or directory opened.
When a file or directory closes, then a final USN record is generated with the USN_REASON_CLOSE flag set. The next change (for example, after the next open operation or deletion) starts a new record with a new set of reason flags.

This implies that duplicate events in the context of an open file’s lifetime can be combined into a single bit in the Reason mask: USN_REASON_DATA_EXTEND can only be set once per record, so an I/O pattern that consists of an open, two writes, and a close will only indicate that some write happened, not which or how many. Consequently, the change journal can’t answer detailed questions about the magnitude of I/O on an open resource; only whether or not some events did occur on it. This is not a major deficiency for the purposes of integrity monitoring, however, as we’re primarily interested in knowing when files change and what their end state is when they do.

Bringing the change journal into osquery

The snippets above give us the foundation for retrieving and interpreting change journal records from a single volume. osquery’s use case is more involved: we’d like to monitor every volume that the user registers interest in, and perform filtering on the retrieved records to limit output to a set of configured patterns.

Every NTFS volume has its own change journal, so each one needs to be opened and monitored independently. osquery’s pub-sub framework is well suited to this task:

  • We define an event publisher (NTFSEventPublisher)
  • In our configuration phase (NTFSEventPublisher::configure()), we read user configuration a la the Linux file_events table:carbon
  • The configuration gives us the base list of volumes to monitor change journals on; we create a USNJournalReader for each and add them as services via Dispatcher::addService()
  • Each reader does its own change journal monitoring and event collection, reporting a list of events back to the publisher
  • We perform some normalization, including reduction of “old” and “new” rename events into singular NTFSEventRecords. We also maintain a cache of parent FRNs to directory names to avoid missing changes caused by directory renames and to minimize the number of open-handle requests we issue
  • The publisher fire()s those normalized events off for consumption by our subscribing table: ntfs_journal_events

Put together, this gives us the event-based table seen in the screenshot above. It’s query time!

carbon (2)

Wrapping things up

The ntfs_journal_events table makes osquery a first-class option for file monitoring on Windows, and further decreases the osquery feature gap between Windows and Linux/macOS (which have had the file_events table for a long time).

Do you have osquery development or deployment needs? Drop us a line! Trail of Bits has been at the center of osquery’s development for years, and has worked on everything from the core to table development to new platform support.