Runtime Verification August 2023 Updates

Welcome to another issue of our monthly newsletter on Medium. This time around, we bring our updates for the month of August. As always, the updates that we post here are summarized and simple, but we are more than happy to give more details and answer any questions on our Discord server.

AUDITS

During August, we wrapped up several audits, including Zivoe’s audit. We will publish a total of two reports and a blog post for the audit in the upcoming weeks on our Twitter account.

KONTROL (PREV. K-FOUNDRY)

These are the monthly updates from our team working on Kontrol:

• New proof digest system. We now store proofs with a human-readable identifier. This makes it more convenient for users to inspect different versions of a smart contract’s KCFG.
• Changes have been made to avoid footguns when Solidity is converted to K. Contract names containing an underscore or methods clashing with K reserved keywords such as “claim” should not be an issue anymore.
• Fixed several issues that caused crashes during verification via improved handling of Matching Logic predicates.
• Pyk can now handle `#Bottom` and `#Top` responses from the backend without crashing.
• Added support for more Solidity types: Kontrol now allows variables of all static `bytes1..32` and `int8..256` types to be used as function arguments.
• Parallelized the compilation process invoked via `kevm foundry-kompile`, which significantly improves the execution time of this command.
• Added `foundry-merge-nodes` functionality, which lets users merge back two branches after they have been split; in turn, improving the efficiency of the verification. Can be used as `kevm foundry-merge-nodes [Contract.test_name] — node [node id] — node [node id]`.

K-FRAMEWORK

We also bring some updates regarding our K efforts:

• Fixed memory-leaks in Booster when calling LLVM simplifications: dramatically reduced memory usage of long-running Kontrol proofs. Github issue link.
• Added support for Java 18 and up. We removed a dependency no longer available on the newer versions of Java.
• Language wise, we restricted the rule labels to no longer contain ` (backticks) and whitespaces. This makes it more consistent with the other K tools.
• We continued the work on better error messages for attributes. You will now receive more details about which attributes are allowed on modules, productions or rules.

ERCx

And, before wrapping up this month’s newsletter, here are the ERCx updates:

• ERCx can now classify tokens up to 8 ERC standards: ERC-20, ERC-721, ERC-721 TokenReceiver, ERC-1155, ERC-1155 TokenReceiver, ERC-3156 FlashLender, ERC-3156 FlashBorrower, ERC-4626.
• We have made internal improvements to our tools and are preparing several exciting new features for September, when we’ll run a workshop and a talk at ETH Chicago.

That’s all for this month’s updates. Stay tuned and join us in Discord to not miss any news from us.