netidee
EtherTrust
EtherTrust - Trustworthy smart contracts

EtherTrust

Förderjahr 2017 / Project Call #12 / ProjectID: 2158

EtherTrust ist ein Analysetool für Ethereum smart contracts. Smart contracts sind Programme, die in der Kryptowährung Ethereum Finanzflüsse steuern. Fehlerhafte oder bösartige contracts können den Nutzer viel Geld kosten – im Vorfeld ist das jedoch kaum zu erkennen. Hier hilft EtherTrust: Auf einer intuitiven Website können Nutzer contracts, die sie verwenden wollen, analysieren. So können sie mit Sicherheit ausschließen, dass ein contract bestimmte gefährliche Eigenschaften hat – dafür gibt es eine bewiesene Garantie.

EtherTrust is an analysis tool for Ethereum smart contracts. Smart contracts are programs that control money flows in the crypto currency Ethereum. Faulty or malicious smart contracts can make users loose a lot of money - spotting such contracts in advance however is a delicate task. Here EtherTrust comes into play: On an intuitive website, users can analyse those contracts that they want to use. In this way they can make sure that a contract does not show malicious behaviour - EtherTrust provides a reliable guarantee for that.

Summary

summary.pdf
(18.02 KB )

Themengebiet

Blockchain

Zielgruppe

Start-ups
,
thematische Community

Gesamtklassifikation

Client Server Applikation
,
SW-Framework

Technologie

blockchain
,
Java
,
Javascript

Uni | FH [Universität]

Technische Universität Wien

Projektteam

Male avatar
Matteo Maffei
Female avatar
Clara Schneidewind
Male avatar
Niklas Grimm
Male avatar
Ilya Grishchenko

Projektergebnisse

Summary CC-BY

Kurzzusammenfassung des Projektes (Short project summary)

pr2158_Call12_Zusammenfassung_V02_0.pdf
163.07 KB
Zusammenfassung
Website

Website von EtherTrust (website of EtherTrust)

http://secpriv.tuwien.ac.at/tools/ethertrust
EtherTrust
Anwenderdoku CC-BY

Anwenderdokumentation von EtherTrust (user guide)

Einführung in die Funktionsweise der Website für Anwender (Introduction to using the website)

user_guide.pdf
1.36 MB
usere guide
Code GPL 3.0

Github Repository von EtherTrust (GitHub repository of EtherTrust)

https://github.com/SecPriv/EtherTrust
Repository
Entwicklerdoku CC-BY

Entwicklerdokumentation von EtherTrust (developer guide)

Übersicht für Dritte, die EtherTrust weiterentwickeln wollen. (Overview for everyone willing to develop EtherTrust further)

dev_guide.pdf
87.46 KB
developer guide
Paper CC-BY

EtherTrust: Sound Static Analysis of Ethereum bytecode

Technischer Report zur statischen Analyse von Ethereum smart contracts. (Technical report for the static analysis of Ethereum smart contracts)

staticanalysis.pdf
1.01 MB
static analysis
Paper CC-BY

A Semantic Framework for the Security Analysis of Ethereum smart contracts

Technischer Report für die formale Semantik und Sicherheitseigenschaften von Ethereum smart contracts. (Technical report for the formal semantics and security properties of Ethereum smart contracts.)

semantics.pdf
432.45 KB
formal semantics
Paper CC-BY

Foundations and Tools for the Static Analysis of Ethereum smart contracts

Tutoriums- und Übersichtspapier zur statischen Analyse von Ethereum smart contracts. (Tutorial and survey paper on the static analysis for Ethereum smart contracts.)

cav2018.pdf
853.31 KB
cav paper
Präsentation CC-BY

Tutorial: Foundations and Tools for the Static Analysis of Ethereum smart contracts

Tutorium zur statischen Analyse von Ethereum smart contracts (gehalten auf CAV 2018). Tutorial on the static analysis for Ethereum smart contracts (given at CAV 2018)

cav-tutorial.pdf
48.43 MB
cav tutorial
Code GPL 3.0

FStar Implementierung der Small-Step Semantic (FStar implementation of the small-step semantics)

eth_semantics_fstar.zip
2.7 MB
fstar semantics
Zwischenbericht CC-BY

Zwischenbericht des Projektes (midterm report)

prj2158_Call12_Zwischenbericht_V01.pdf
372.1 KB
midterm report
Endbericht CC-BY

Endbericht (final report)

Endbericht zum Projekt EtherTrust (final report for the EtherTrust project)

prj2158_Call12_Endbericht_V01.pdf
434.68 KB
final report
Studie | Bericht | Konzept CC-BY

Dokumentation der Externkommunikation (documentation of external communication)

prj2158_Call12_ExternKommunikation_V01.pdf
366.83 KB
external communication
Client-SW GPL 3.0

EtherTrust Prototype (Binaries)

Erster Prototyp für das Analysetool EtherTrust (Binaries), veraltet. (First prototype of the analysis tool EtherTrust, outdated)

ethertrust_bin.zip
34.01 MB
prototype binaries
Code GPL 3.0

EtherTrust Prototype (Sources)

Erster Prototyp für das Analysetool EtherTrust (Sources), veraltet. (First prototype of the analysis tool EtherTrust, outdated)

ethertrust.zip
20.83 MB
prototype sources

Blogbeiträge

In diesem Beitrag wollen wir euch die Website vorstellen, über die ihr EtherTrust ab jetzt online ausprobieren könnt!

( )
EtherTrust goes online

Das Netidee-Projekt EtherTrust geht dem Ende zu. In diesem Beitrag berichten wir, wie es jetzt weitergeht.

( )
Tschüss!

Um EtherTrust als einverlässliches Tool zu implementieren, haben wir sein Design grundlegend geändert. In diesem Beitrag geben wir einen Überblick über dieses neue Design.

( )
HoRSt

Um die Probleme zu lösen, die wir beim Erstellen des Prototypen von EtherTrust entdeckt haben, haben wir uns entschlossen EtherTrust neu zu designen. Kernstück dieses neuen Designs ist die Spezifikationssprache HoRSt.

( )
Ein neues Design für EtherTrust

EtherTrust beweist allgemeine Sicherheitseigenschaften von Smart Contracts. Um das zu ermöglichen müssen diese Sicherheitseigenschaften aber passend formuliert sein, um sie mit unserer Analyse ausdrücken zu können. Hier zeigen wir, wie man dies mache

( )
Abstrakte Sicherheitseigenschaften

Um die Praktikabilität unseres Ansatzes zu evaluieren implementieren wir einen ersten Prototyp von EtherTrust. Hier beschreiben wir, wie dieser aufgebaut ist.

( )
Erster Prototyp

EtherTrust analysiert Smart Contracts, indem es ihr Ausführungsverhalten in einer logischen Form kodiert, die von einem SMT-Solver verarbeitet werden kann. Dabei müssen jedoch Abstraktionen des Ausführungsverhaltens vorgenommen werden, damit der SMT-

( )
Wie wir unsere Semantik "abstrakter" machen

Beim Erstellen eines ersten Prototyps für EtherTrust sind uns einige Probleme aufgefallen, deren Lösung eine größere Änderung im Design unseres Tools bedarf.

( )
Die Tücken des Prototyps

Um Smart Contracts automatisch analysieren zu können beschreiben wir ihr Ausführungsverhalten in einer logischen Form, die dann von einem automatisieren Lösungsprogramm verarbeitet werden kann. Hier erklären wir, wie diese logische Form aussieht.

( )
Horn Clauses: Futter für den SMT-Solver

EtherTrust analysiert Smart Contracts, in dem es das Ausführungsverhalten von Verträgen in einer logischen Form - sogenannten Horn clauses - beschreibt. Hier beschreiben wir, wie man aus der formalen Semantik von Ethereum Smart Contracts eine solche

( )
Von der Semantik zu Horn Clauses

Ausschnitt aus der FStar Implementierung unserer Semantik
Um sicher zu stellen, dass unsere mathematischen Modelle auch wirklich beschreiben, was in der Realität passiert müssen wir sie testen. Wie wir das für EtherTrust machen beschreiben wir hier.

( )
Theorie und Praxis

Bisher haben wir schon über die Semantik von Smart Contracts uns über Sicherheitseigenschaften berichtet. Als nächstes geht es nun um die automatische Analyse von Smart Contracts. Was dafür nötig ist und wie das mit den bisherigen Arbeitsschritten zu

( )
Roadmap

Im Juli haben wir bei der ,Federated Logic Conference' in Oxford ein Tutorium zu EtherTrust gegeben und unsere bisherige Arbeit vorgestellt.

( )
Tutorium bei FLoC

Fehlerhafte Smart Contracts wie der DAO Contract haben zu großen finanziellen Verlusten geführt. Aber wie kann man allgemein beschreiben, wann ein Smart Contract fehlerhaft ist?

( )
Sicherheitseigenschaften von Smart Contracts - Formal!

Bei der diesjährigen Konferenz ETAPS in Thessaloniki haben wir unser wissenschaftliches Papier ,A Semantic Framework for the Security Analysis of Ethereum Smart Contracts' vorgestellt und sogar einen Best Paper Award dafür erhalten

( )
Das EtherTrust-Team bei ETAPS in Thessaloniki

Um Smart Contracts auf ihre Sicherheit testen zu können, muss man zunächst verstehen, was denn die existierenden Sicherheitsprobleme sind. Wir erklären hier einen bekannten Angriff - den sogenannten theDAO hack.

( )
Sicherheitsprobleme in Smart Contracts

Bytecode in Hexadezimaldarstellung
Ethereum Smart Contracts werden in einer speziellen, maschinennahen Programmiersprache geschrieben - EVM Bytecode. Wie diese Sprache aussieht, warum wir sie analysieren wollen und in welchen Programmiersprachen Entwickler tatsächlich Smart Contracts

( )
EVM Bytecode

Um verstehen zu können, wie Smart Contracts funktionieren und was bei ihrer Entwicklung alles schief gehen kann, ist es wichtig ein grundlegendes Wissen über die Funktionsweise von Kryptowährungen (in unserem Fall insbesondere Ethereum) zu haben. In

( )
Ethereum

Wie kann man eigentlich gewährleisten, dass eine Tool beweisbare Garantien liefert? Und was kann dabei alles schief gehen?

( )
Der mathematische Kern von Ethereum smart contracts

Ähnliche Projekte

Wir sind ein Team aus Computerwisschenaftlern, das es sich zum Ziel gesetzt hat, den Zugang und Einstieg zu Data-Science möglichst einfach zu gestalten. Dr. Stefan Gindl: Senior-Data-Scientist und Software-Developer Yasin Ghafourian: PhD-Researcher

PrototAIp

Die Motivation hinter dem Projekt ist es die Entwicklung und den Betrieb eines IoT-Systems zu vereinfachen. Dabei ist das Ziel ein Baukastensystem für Hardware, Datentransport und Sicherung zur Verfügung zu stellen.

Open³ Toolbox

Phishing ist ein bis heute ungelöstes Problem. Wir verbinden Technik mit Psychologie und wollen Phishing mit Hilfe einer neuartigen Awareness-Strategie besiegen. Vorrangige Zielgruppe sind SchülerInnen zwischen 14 -18 Jahren.

Phishingtraining

MSS network map.
Das Macroseismic Sensor (MSS) Netzwerk ist ein dichtes Netzwerk seismischer low-cost Sensoren, die in besiedelten Gebieten mit sensitiver Infrastruktur aufgestellt sind.

MSS Outreach

Internet security
Client- und Server-seitige Software Bibliotheken für EntwicklerInnen zur Gewährleistung einer sicheren und nachvollziehbaren Datenübertragung!

SIKOSI

Datenschutzinformation
Impressum | Datenschutz
Der datenschutzrechtliche Verantwortliche (Internet Privatstiftung Austria - Internet Foundation Austria, Österreich) würde gerne mit folgenden Diensten Ihre personenbezogenen Daten verarbeiten. Zur Personalisierung können Technologien wie Cookies, LocalStorage usw. verwendet werden. Dies ist für die Nutzung der Website nicht notwendig, ermöglicht aber eine noch engere Interaktion mit Ihnen. Falls gewünscht, treffen Sie bitte eine Auswahl:
Sonstige Inhalte (1 Dienst)
Einbindung zusätzlicher Informationen
YouTube
Google Ireland Limited, Irland
Alle Detailszu YouTube
Alle Detailszu YouTube