Ich trete Ethereum als formeller Überprüfungsingenieur an. Meine Argumentation: Die formelle Überprüfung ist als Beruf nur in einer seltenen Situation, wo
- Das Überprüfungsziel folgt kurze, einfache Regeln (EVM);
- Das Ziel trägt viel Wert (ETH und andere Token);
- Das Ziel ist schwierig genug, um richtig zu werden (jedes nicht triviale Programm);
- Und die Community ist sich bewusst, dass es wichtig ist, sie (vielleicht) richtig zu machen.
Mein letzter Job als formeller Überprüfungsingenieur hat mich auf diese Herausforderung vorbereitet. Außerdem habe ich in der Nähe von Ethereum mit zwei Projekten gespielt: einen Online -Service namens Der Ethereum Contract Analyzer von Dr. Y. Und Ein Github -Repository mit CoQ -Proofs enthält. Diese Projekte befinden sich an den entgegengesetzten Extremen eines Spektrums zwischen einem automatischen Analysator und einer manuellen Nachweisentwicklung.
In Anbetracht der kollektiven Auswirkungen auf das gesamte Ökosystem bin ich von einem automatischen Analysator angezogen, der in einen Compiler integriert ist. Viele Leute würden es leiten und einige würden seine Warnungen bemerken. Auf der anderen Seite sollte überraschend ein überraschendes Verhalten als Fehler angesehen werden, aber die Überraschung sollte entfernt werden, aber Computer können die menschlichen Erwartungen nicht spüren. Um den Maschinen die menschlichen Erwartungen zu erzählen, sind einige manuelle Anstrengungen erforderlich. Die Vertragsentwickler müssen den Vertrag in einer maschinenlesbaren Sprache angeben und den Maschinen Hinweise geben, warum die Implementierung der Spezifikation übereinstimmt (in den meisten Fällen möchte die Maschine immer mehr Hinweise, bis der Mensch einen Fehler realisiert, häufig in der Spezifikation). Dies ist arbeitsintensiv, aber solche manuellen Anstrengungen sind gerechtfertigt, wenn ein Vertrag für mehreren Millionen Dollar ausgelegt ist.
Eine Person, die sich den formellen Methoden widmet, gibt uns nicht nur die Möglichkeit, uns in diesem wichtigen Bereich schneller zu bewegen, sondern auch fruchtbar, sondern ermöglicht es uns hoffentlich auch, mit der Wissenschaft besser zu kommunizieren, um die verschiedenen einzigartigen Projekte zu verbinden, die in den letzten Wochen erschienen sind.
Hier sind einige Projekte, die wir in Zukunft angehen möchten. Die meisten werden wahrscheinlich in Zusammenarbeit mit anderen Teams durchgeführt.
Solidität:
- Erweitern Sie die Solidität auf die WHY3 -Übersetzung auf die vollständige Soliditätssprache (wechseln Sie möglicherweise zu F*)
- formale Spezifikation der Solidität
- Syntax und Semantik der modalen Logik für die Argumentation über mehrere Parteien
Gemeinschaft:
- Erstellen einer Karte formeller Überprüfungsprojekte auf Ethereum
- Sammeln von Buggy Solidity Codes zum Benchmarking automatischer Analysatoren
- Analyse von Einsatzverträgen auf der Blockchain für Schwachstellen (verwandte: Werkzeughörer)
Werkzeuge:
- Bieten Sie eine menschliche und maschinenlesbare Formalisierung des EVM an, die auch ausgeführt werden kann
- Entwicklung formell verifizierter Bibliotheken in EVM -Bytecode oder Solidität
- Entwicklung eines formell verifizierten Compilers für eine winzige Sprache
- Erforschen Sie das Potenzial für interaktionsorientierte Sprachen (“Wenn X passiert, dann tun Sie y; Sie können nur z tun, wenn Sie ein” gemacht haben “).
