@sxysun there's also a WIP isabelle semantics of yul that are further along than the
yul-semantics mentioned above in some regards. Check it out here https://github.com/mmalvarez/Yul-Isabelle
Wonderful! The formalized semantics could really help. And just to clarify, @chriseth isn't the EVM dialect of Yul with https://solidity.readthedocs.io/en/develop/assembly.html#opcodes as builtin functions the same as https://solidity.readthedocs.io/en/develop/yul.html#low-level-functions except they do not have types?
if anybody is interested in encoding the Solidity memory model into SMT, we have a new paper out describing how we do it in solc-verify. draft preprint available at https://arxiv.org/abs/2001.03256. any comments and suggestions very welcome.
not really, i'm not 100% with understanding the semantics of function types yet. also i'm not sure who's using them, why and how. seems like a lot of work to support properly, basically encode the integer value and then do manual dispatch. we just ignore for now. are there any interesting contracts that use it in practice?
Tomorrow Algorand is hosting a live webinar on implementing the world’s first CBDC. I have submitted a few questions and will be attending. This is a great way to spend your quarantine :)
Register and submit questions here: https://register.gotowebinar.com/register/5273854108710515471
There will be 3 PLDI talks devoted to smart-contract analysis / verification at 19 Jun. Check https://pldi20.sigplan.org/program/program-pldi-2020 for details. PLDI is online and free this year due to well known circumstances.
FYI: There will be a workshop on smart contract analysis techniques, including sound techniques soon. They still accept papers btw https://conf.researchr.org/track/issta-2020/issta-2020-wosca
@unboxedtype I haven’t tried myself, but you can take a look here https://github.com/boogie-org/boogie/blob/032700096179f5af1be4c50dd5ed8afb6b361e09/Test/smack/git-issue-203.bpl#L55. You should try and avoid if possible.
hevm now supports symbolic execution of EVM bytecode!
https://fv.ethereum.org/2020/07/28/symbolic-hevm-release/
https://fv.ethereum.org/2020/07/28/symbolic-hevm-release/
@leonardoalt Hi! I came across your issue in Z3 github related to proofs verification generated by Z3. Are you guys or someone you might know working on this problem? Seems like Z3 still does not implement proof checking in full. Other related SMT-proof-checking tools also avoid Z3 for some reason.
xvwx @leo put together a very nice overview here: https://github.com/leonardoalt/ethereum_formal_verification_overview
xvwx in terms of tools deployed in the wild, I would say that the k framework has seen the most usage
Maybe someone is interested, today we will present our paper 'eThor: Practical and Provably Sound Static Analysis of Ethereum Smart Contracts' at CCS (https://www.sigsac.org/ccs/CCS2020/). The paper is also available at https://arxiv.org/abs/2005.06227
don't know if this is the right place to ask this question, but i'm trying to look through all chain data to see how many contracts use
BLOCKHASH for randomness (related to eth1+eth2 merge research) and had the idea of looking for bytecode where the blockhash is subsequently hashed to an int. anyone know if there's a rigorous way to do this search?
We integrated hevm's symbolic execution features into its unit testing framework. This lets you formally verify properties directly in Solidity, using almost exactly the same syntax as writing a property based test.
More details here: https://fv.ethereum.org/2020/12/11/symbolic-execution-with-ds-test/#setting-up-the-environment
Hey, I just saw that in the git repo Lolisa is commented as having no work developed after 2018 but I'd consider this https://ieeexplore.ieee.org/stamp/stamp.jsp?arnumber=8970279 a development in the verification framework and Lolisa
After reading that paper does anyone have any reasons on why this isn't the most up to date, intuitive and versatile tool for ETH formal verification (provided that the tool actually exists since there's no open source code)
<Hudson Jameson (souptacular)> This formal-methods channel is now bridged between Gitter (https://gitter.im/ethereum/formal-methods) and the Eth R&D Discord server under the
ETH2-RESEARCH section. Enjoy!
<jc> Discord link for others https://discord.gg/N8szq4J8Gt