Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Activity
  • Oct 21 2017 21:21
    @jpitts banned @Musk55
chriseth
@chriseth
@sxysun there are some other small differences, but essentially yes
Sumit Lahiri
@codersguild
We are actively working on making a theorem solver that runs on a blockchain and can be used to verify a wide range of smart contracts.
chriseth
@chriseth
@codersguild nice! Is it bytecode- or high-level-language based?
Sumit Lahiri
@codersguild
High-level language as of now but will soon move to EVM bytecode.
Evgeniy Shishkin
@unboxedtype
@codersguild Hi! By theorem solver you mean some form of SMT-solver or automatic theorem prover, like Vampire et al? Do you have any materials on the subject?
Dejan Jovanović
@dddejan
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.
Leonardo
@leonardoalt
@dddejan nice, thanks for sharing the paper. Do you have any plans for function types? I'm currently only abstracting them as integers, without reasoning properly about them.
Dejan Jovanović
@dddejan
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?
Leonardo
@leonardoalt
not that I know, I also think it's not really worth it for now
Dejan Jovanović
@dddejan
for example, seems complicated to figure out given a function type which internal functions can be called and what are their values.
chriseth
@chriseth
@dddejan without having read the paper - do you have any feedback concerning language or compiler design?
River
@endorphin
@leonardoalt @MrChico requesting push access for git@github.com:ethereum/act.git
Leonardo
@leonardoalt
@endorphin sent invite
Dejan Jovanović
@dddejan
@chriseth we do have some thoughts. mainly things that makes semantics very complicated or very diffucult to analyze.
chriseth
@chriseth
please feel free to pour specific suggestions into issues on github.com/ethereum/solidity !
Dejan Jovanović
@dddejan
can do, it's a good idea. at least to get a rationale for some of the design decisions that are probably driven by practicall issues we don't see.
Ada922
@Ada922

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

Greg Colvin
@gcolvin
This would be Naveed’s work with the Marshall islands. Interesting stuff.
Evgeniy Shishkin
@unboxedtype
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.
Leonardo
@leonardoalt
Thanks @unboxedtype !
Evgeniy Shishkin
@unboxedtype
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
Evgeniy Shishkin
@unboxedtype
Hey Boogie experts, how to convert bit vector into int and probably other way around?
Dejan Jovanović
@dddejan
@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.
Evgeniy Shishkin
@unboxedtype
@dddejan Thanks a lot!
MrChico
@MrChico
hevm now supports symbolic execution of EVM bytecode!
https://fv.ethereum.org/2020/07/28/symbolic-hevm-release/
Ben Siraphob
@siraben
@MrChico Will symbolic execution be able to detect bugs caused by integer over/underflow?
MrChico
@MrChico
@siraben not directly with this release, but if you add overflow checks like assert(x + y >= x), it would
Ben Siraphob
@siraben
@MrChico I see.
Evgeniy Shishkin
@unboxedtype
@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.
Leonardo
@leonardoalt
@unboxedtype we're not working directly on proof checking. We would like to have it though, since it would be necessary in case the Solidity compiler decides to use SMT solvers for Yul optimization
Evgeniy Shishkin
@unboxedtype
@leonardoalt Got it, thanks!
0xVerif
@0xverif
Hey, I'm researching formal methods for smart contracts on Ethereum for my masters degree thesis, does anyone have an index summarizing research on this area? And/or an opinion on leading projects and research? Thanks a lot!
matrixbot
@matrixbot
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
0xVerif
@0xverif
Thank you!
ylya
@ylya
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
Leonardo
@leonardoalt
@ylya thanks! Could you also share here what time that will be?
ylya
@ylya
@leonardoalt Gladly :) The session starts at 2:30 Eastern Standard Time (UTC -5:00), in ~4 hours
Lakshman Sankar
@lsankar4033
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?
Lakshman Sankar
@lsankar4033
my very not formal idea that i'm starting with is just filtering out contracts where there's a SHA3 N opcodes after BLOCKHASH for some N
xvwx
@xvwx:matrix.dapp.org.uk
[m]

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

0xVerif
@0xverif
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)
Eth-Gitter-Bridge
@Eth-Gitter-Bridge
<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!
Eth-Gitter-Bridge
@Eth-Gitter-Bridge
<jc> Great thx Hudson!
<jc> Discord link for others https://discord.gg/N8szq4J8Gt
ocschwar
@ocschwar
Happy new year all
Eth-Gitter-Bridge
@Eth-Gitter-Bridge
<arseniy> Is this a good place to ask questions about using the SMTChecker in Solidity 0.8.3?
Eth-Gitter-Bridge
@Eth-Gitter-Bridge
<Micah> https://forum.soliditylang.org/ would probably be a better place to go for that.
Leonardo
@leonardoalt
@adklempner (hope I tagged the right person) here's ok if you wanna have a sync chat, but the forum is also fine!