Runtime Verification May 2023 Updates

Welcome to another issue of our monthly newsletter on Medium. This time around, we bring our updates for the month of May. 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 May, we wrapped up several audits including Morpho’s AAVE v3 protocol. A technical report has been published and a blog post will be coming up in the upcoming weeks. We also published a blog post about the audit we conducted on the Proof of Neutrality Network last month. We have completed several other audits and we will be announcing them soon on our Twitter account.

BLOG POSTS

We published a piece co-authored with Term Labs about how a 2-week audit resulted in a new simplified algorithm to improve code efficiency. The blog post deep dive into how both teams closely collaborated to not only create a new optimized “clearing price” algorithm but also to make sure that the original algorithm was properly analyzed.

EVENTS

For this month, we have two small updates regarding events. While Ilja, one of our formal verification engineers, attended Edcon and Grigore and Yale attended Consensus earlier this month, Andrei Vacaru got a talk submission accepted at EthBelgrade on June 4th about how to start symbolically testing your code using KEVM integration for Foundry.

KEVM + FOUNDRY

These are the monthly updates from our team working on KEVM + Foundry:

• KEVM Port kompilation logic from Bash script / Makefile to Python.
• KEVM has a changed import structure which allows users to include automatically generated modules with symbols for EVM bytecode and jump destinations for a particular contract, making, e.g., circularity rules more stable with contract changes.
• KEVM now stores digests of the input Foundry files. This means that it will auto-detect if rekompilation of the K file is needed when calling `kevm foundry-kompile …` on your project!
• A number of useful lemmas about arithmetic, bitwise, and byte-related reasoning, which have arisen from various verification engagements, have been merged into KEVM, improving its out-of-the-box symbolic reasoning. Further lemmas are expected to be introduced in the coming months.
• KEVM’s handling of gas semantics, especially infinite gas for symbolic reasoning, has been improved so that we can have simpler and faster symbolic reasoning.
• Gitbook created for KEVM Foundry Integration (https://runtime-verification-tooling.gitbook.io/kevm-integration-for-foundry/) with steps on how to use the integration and will be updated with additional technical uses. Github integration with Gitbook has been set up (https://github.com/runtimeverification/gitbook-kontrol) this will allow comments/changes to be submitted through Github issues and PRs.
• Better error messages when KEVM is used without arguments.
• The contract compiling process is now included in the `foundry-kompile` command. This means that running `forge build` is no longer required.

K- FRAMEWORK

We also bring some updates regarding our K efforts:

• Research into accelerated symbolic execution is progressing well. Our new (closed-source) execution server delivers consistent speedups >2.5 (compared with kore-rpc of the open-source Haskell backend) on a range of foundry test cases, and additional optimizations are in progress which will unlock further speedups.
• Cleaned up the help options for the K tools. The advanced options have been moved to ` — help-hidden`. This should make it easier for new users to find the most commonly used parameters.
• Added more checks for `left`, `right` and `non-assoc` attributes.
• Added a new option ` — pedantic-attributes` to help users distinguish between built-in attributes and user-defined ones. User-defined ones need to be added as a parameter to the `group` attribute. These can later be used to specify priorities and associativity.
• The `total` attribute can now be added only to productions that are also `function`.

ERCx

ERCx homepage

These are the updates from the ERCx team:

• Migrate code to RV Python project template: consistent formatting, use of linters and type checker.
• Consolidation of ERC 4626 inside our library. (They should make it to the website in a week or so).
• More efficient ABI tests. In our always-on effort to improve the quality of our test suite, we have factored our ABI tests. In essence, the code of our ABI tests is more modular and provides more precise feedback to the user.
• Detecting when a token is behind a proxy. We are now able to detect when a token uses a proxy contract to its implementation. This allows us to evaluate more tokens, while tokens behind proxies were not evaluable by our test suite.
• Added Fingerprint tests. We have added tests to a new category called Fingerprint. Tests in the category “Fingerprint” are neither good nor bad properties to have but instead indicate the implementation choice made for the token. These can be useful when understanding a token behavior.

• Internal improvements. We have also brought fixes and updates to ERCx to make it more robust and easier to install.
• Added scores to facilitate the quick evaluation of a token. As a result of our tests, we produce a multi-dimensional score to reflect how a token performs against our test suite. Our score can be decomposed as follows:
  - A global score reflecting how many tests pass.
  - A multi-dimensional score where tests are categorized into topics (e.g., approval, transfer) and where we count the number of passing tests for each category. Such a score will be useful for comparing tokens (a feature we will bring soon to ERCx).
• In collaboration with Certora (Chandrakana Nandi), we have submitted a paper to FSE industry track on the combined use of Gambit with ERCx. More precisely, we explore the benefits of mutation testing in (1) improving the quality of our test suite and ensuring its completeness and (2) discovering properties of the Ethereum ecosystem on mutants, understanding the relationship between properties and bugs.

URBIT: HOON PROPERTY TESTS AND K INTEGRATION

We are introducing updates related to the Urbit Grant our team is working on:

• Work has started on the grant: https://urbit.org/grants/kNock-property-testing. We are calling the library “quiz”
• We have an open pull request (https://github.com/urbit/urbit/pull/6558) with all the essential functionality implemented:
  - You can easily pass a test from the command line and the tool will run it for you with randomized inputs.
  - You can also use it in the regular Urbit testing library, and then you can pass it your own ways to create random inputs, rather than relying on the built-in random generation.
  - You can drop certain inputs and ask to re-generate instead.
  - If a failing input is found, it can be “shrunk”: the library will search for the smallest possible input that would cause the failure.
• We are still in the prototype phase. The library can’t currently generate examples for some types of inputs. It works for basic types like integers, cells and union types, but not for advanced types that rely on more advanced polymorphism in Hoon, such as lists or cores.

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