1. 8
  1. 3

    Nice overview. I recommend adding Runtime Verification Inc’s work under verification given what they’re doing will be more accessible than Coq. For instance, their RV-Match tool is push-button with low, false positives. I’m not sure if they have one like that for Ethereum contracts. If not, they’re probably working on it now. They have a list of successful work on their page and blog.

    Also, their K Framework is open source for folks to build on.

    1. 3

      Runtime Verification Inc has done fantastic work.

      I am happy that they worked on semantics for smart contract languages like Vyper & Solidity.

      1. 3

        Wait, I forgot that @lojikil works at a company that built Manticore and Slither. Manticore does symbolic execution on smart contracts. Slither does static analysis on Solidity code. Both are AGPLv3 with commercial licenses available. Since I don’t do smart contracts, I can’t tell you any more than that. :)

        Trivia: Slither’s name was chosen after they held a focus group asking project managers and finance experts to visualize things that helped them sleep at night. That’s because the product was supposed to help them sleep at night. They arrived at Slither. Some outsiders were baffled at the result.

        Trivia: The above trivia may or may not be a work of fiction. Its author is skeptical about the user considerations that went into choosing the name, though. ;)

        1. 2

          tl;dr: there’s lots of formal verification going on in the space, and lots of collaboration too, and regardless of what anyone thinks of cryptocurrency and smart contracts, it’s super interesting to see the space evolve

          The RunVer folks do some great work with K; K for EVM, for eWASM, for client projects, it’s pretty interesting. The ChainSecurity folks also have SOLTIX and VerFx (I think, the name eludes me, I still haven’t processed coffee) for testing Solidity compilers and smart contracts respectively. Likewise, the Consensys Diligence folks have Mythril Classic, their new MythX platform, and a few other things.

          On our side, we have a suite of tools we’ve released. Beyond what Nick mentioned, these include:

          Also, Slither contains an IR called “SlithIR”, which we use internally for additional tooling. There’s also work on symbolic computation & abstract interpretation atop SlithIR.

          Regardless of what you think of the space, the thing I find most fascinating is that there are several companies working in the formal verification space and helping clients really understand the correctness of the code they’ve written. This means understanding the semantics of terrible languages like Solidity (and better ones like Vyper, hi Bryant!), the EVM, contributing to discussions like “should we add static jumps to EVM” or “Is you gas calculation horribly broken?”. You’ll note the EIP-1283 link is a collaboration between ToB, ChainSecurity, and the Eveem teams; many companies just show up and collaborate to make things better.

          1. 3

            Thanks for detailed reply!

            “regardless of what anyone thinks of cryptocurrency and smart contracts, it’s super interesting to see the space evolve”

            Heck yeah, it is. I call out cryptocurrency and blockchains as mostly useless. Yet, the cryptocurrency verification scene is awesome. Between it and CompSci’s latest, we’re in a golden age of applied, formal verification being able to have an impact in the world. My recommendation was people learn verification, start in these companies (or start companies), and build on existing tools with lots of academic collaboration to make them cover more use cases. Aka, leverage the piles of money to build what they want along with what we all need. Although most focus on proof, I like that you have a mix of tools including testing and verification, HLL’s and binary. That’s consistent with high-assurance security using a mix of tools to cover any’s weaknesses. Smart.

            That leads to only gripe I have in this space. Aside from RVI w/ K, what few I’ve seen aren’t building on the tools that already have strong ecosystems. That includes Why3 (esp Why3), Simpl w/ HOL used in seL4 (eliminates compiler), whatever CakeML people are using, ACL2, KLEE, and so on. As each extension happens, we would get new theories or plugins that cover certain kinds of properties that others can reuse. Why3 (software) and ACL2 (hardware) crowds were doing this the most with lots of automation (good for accessibility). That’s what I want to see more of. Then, maybe spec/property-based, test generation supported for each thing they contribute to empirically test the proven code. Eventually, we have toolchains that can handle about anything really critical.

            The crypto-verification communities are doing lots of good work. They have even more potential than that, though. The kind of potential that kicks off future projects in unrelated areas. That’s what I want to see next.