christoftorres / osiris Goto Github PK
View Code? Open in Web Editor NEWA tool to detect integer bugs in Ethereum smart contracts (ACSAC 2018).
osiris's People
Contributors
Stargazers
Watchers
Forkers
yra40 hnyuuu kunpengren m3terpreter metaver5o carloscerq purathani xyunsh 5l1v3r1 ljhofgithub omelancon backroadtech zhidandengosiris's Issues
Osiris finds no bugs in example Division.sol contract
Hello,
When I try to test the Division.sol contract with the Docker, Osiris does not find any bugs (even after uncommenting the first function). Why?
I used this command inside the docker:
python osiris/osiris.py -s datasets/Division/Division.sol
contract Division {
function unsigned_division(uint32 x, uint32 y) returns (int r) {
//if (y == 0) { throw; }
r = x / y;
}
function signed_division(int x, int y) returns (int) {
//if ((y == 0) || ((x == -2**255) && (y == -1))) { throw; }
return x / y;
}
}
The result:
.oooooo. o8o o8o
d8P' `Y8b `"' `"'
888 888 .oooo.o oooo oooo d8b oooo .oooo.o
888 888 d88( "8 `888 `888""8P `888 d88( "8
888 888 `"Y88b. 888 888 888 `"Y88b.
`88b d88' o. )88b 888 888 888 o. )88b
`Y8bood8P' 8""888P' o888o d888b o888o 8""888P'
INFO:root:Contract datasets/Division/Division.sol:Division:
INFO:symExec:Running, please wait...
INFO:symExec: ============ Results ===========
INFO:symExec: EVM code coverage: 99.4%
INFO:symExec: Arithmetic bugs: False
INFO:symExec: └> Overflow bugs: False
INFO:symExec: └> Underflow bugs: False
INFO:symExec: └> Division bugs: False
INFO:symExec: └> Modulo bugs: False
INFO:symExec: └> Truncation bugs: False
INFO:symExec: └> Signedness bugs: False
INFO:symExec: Callstack bug: False
INFO:symExec: Concurrency bug: False
INFO:symExec: Time dependency bug: False
INFO:symExec: Reentrancy bug: False
INFO:symExec: --- 1.09610509872 seconds ---
INFO:symExec: ====== Analysis Completed ======
How many integer errors can Osiris detect today?
Hello, I am a postgraduate student from Hohai University. I'm investigating the current smart contract detection tools, and I've read OSIRIS papers. Could you tell me that the types of integer errors that OSIRIS can detect are still the three mentioned in this paper?
running Osiris using the latest Z3
Hi, I am trying to run Osiris using the latest version of Z3 (v 4.8.4).
However, Osiris produces the following error message:
Traceback (most recent call last):
File "osiris/osiris.py", line 10, in <module>
import symExec
File "/home/sunbeom/Osiris/osiris/symExec.py", line 14, in <module>
import z3
File "/home/sunbeom/Osiris/osiris/z3/__init__.py", line 1, in <module>
from .z3 import *
File "/home/sunbeom/Osiris/osiris/z3/z3.py", line 44, in <module>
from . import z3core
File "/home/sunbeom/Osiris/osiris/z3/z3core.py", line 732, in <module>
_lib.Z3_get_parser_error.restype = ctypes.c_char_p
File "/usr/lib/python2.7/ctypes/__init__.py", line 379, in __getattr__
func = self.__getitem__(name)
File "/usr/lib/python2.7/ctypes/__init__.py", line 384, in __getitem__
func = self._FuncPtr((name_or_ordinal, self))
AttributeError: /usr/lib/libz3.so: undefined symbol: Z3_get_parser_error
I tested on Ubuntu 18.04.2 .
My attempt to install the latest Z3 using the docker image provided by you also failed.
problems about web3
could you tell me which version of your web3?
i can't download web3 through pip install, and web3 need the enviroment >=python3.5
thank you
Disabling detection of truncation and signedness bugs
Is it possible to disable the detection of truncation and signedness bugs in Osiris? That is, I would like to use Osiris for detecting only integer over/underflows and division by zeros.
Is it provided by an option currently? (maybe the option "-m"?)
If yes, can you give me some examples?
DeprecationWarning: This library has been renamed to `eth-utils`. The `ethereum-utils` package will no longer recieve updates. Please update your dependencies accordingly.
When I ran Osiris, I got this error message
Traceback (most recent call last):
File "osiris/osiris.py", line 10, in <module>
import symExec
File "/home/hyt/smartsheild/Osiris/osiris/symExec.py", line 30, in <module>
import web3
File "/home/hyt/.local/lib/python2.7/site-packages/web3/__init__.py", line 5, in <module>
from web3.main import Web3
File "/home/hyt/.local/lib/python2.7/site-packages/web3/main.py", line 3, in <module>
from eth_utils import (
File "/home/hyt/.local/lib/python2.7/site-packages/eth_utils/__init__.py", line 2, in <module>
"This library has been renamed to `eth-utils`. The `ethereum-utils` "
DeprecationWarning: This library has been renamed to `eth-utils`. The `ethereum-utils` package will no longer recieve updates. Please update your dependencies accordingly.I felt like Osiris is depending on a lower version of python libraries (web3 and ethereum-utils), which finally leads to this error.
Could anyone help me with this?
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.