From stack to structure: decompiling Ethereum smart contracts via static program analysis

Abstract

Ethereum-based blockchains have been the de facto option for programmable blockchains for over a decade. Ethereum's general and low-level runtime, the Ethereum Virtual Machine (EVM), enabled the rapid development of an ecosystem of decentralized applications built using smart contracts deployed on the blockchain. Security is a major consideration in such a domain as smart contracts can be interacted with by any other on-chain entity, and exploits resulting in significant financial losses are not uncommon. However, the EVM's low-level nature also introduces a new challenge: it was not made to facilitate human understanding and automated analyses. As a contract's EVM bytecode is its only available on-chain artifact, it is crucial to create automated tooling to better understand it. In this thesis we design and employ over-approximate static analysis techniques to create a decompilation pipeline that enables reverse engineering and downstream program analyses. Our decompilation pipeline progressively abstracts away compilation artifacts introduced by compiling high-level source code to EVM bytecode, recovering the higher-level constructs. The contributions of this thesis are split into two parts. The first part focuses on recovering a structured intermediate representation with functions, register variables, and resolved control-flow edges from the low-level stack-based bytecode lacking all the above. In the second part of this thesis, we use that representation in order to enrich it with additional information about the objects stored in the EVM's various heap-like stores. A recurring theme in the contributions in the first part of this thesis is the use of domain-tailored context-sensitivity variants to compute the program's control-flow graph (CFG) in a precise, complete, and scalable manner. This context-sensitive CFG is then used to recognize public and private functions in the unstructured input. Along with other presented techniques such as the cloning of low-level blocks, our lifter was successfully evaluated against state-of-the-art academic and industrial tools.In the second part of this thesis we focus on modeling the EVM's stores. We first focus on ``memory'', a transient store used for inter-contract communication, computing cryptographic hashes, and more. All of these high-level constructs are compiled down to memory store and load instructions, operating on low-level pointers. We design an analysis recovering high-level information and manage to model over 92% of low-level store and load instructions. Our last contribution focused on recovering structure in the EVM's persistent storage. We design and implement an analysis that recovers the arbitrarily nested data structures residing in storage, managing to surpass the state-of-the-art in all axes (scalability, precision, and completeness) while often inferring more structures than the compiler-produced metadata. We also show how the modeling of memory and storage is instrumental for many downstream analyses.

Τα blockchain που βασίζονται στο Ethereum αποτελούν εδώ και πάνω από μία δεκαετία την de facto επιλογή για προγραμματιζόμενα blockchains. Το γενικής χρήσης και χαμηλού επιπέδου περιβάλλον εκτέλεσης του Ethereum, η Ethereum Virtual Machine (EVM), επέ-τρεψε την ταχεία ανάπτυξη ενός οικοσυστήματος αποκεντρωμένων εφαρμογών που υλο-ποιούνται μέσω έξυπνων συμβολαίων και αναπτύσσονται στο blockchain. Η ασφάλεια αποτελεί μείζον ζήτημα σε αυτόν τον χώρο, καθώς τα έξυπνα συμβόλαια μπορούν να αλληλεπιδράσουν με οποιαδήποτε άλλη οντότητα εντός του blockchain, και οι εκμεταλλεύσεις ευπαθειών που οδηγούν σε σημαντικές οικονομικές απώλειες δεν είναι σπάνιες. Ωστόσο, η χαμηλού επιπέδου φύση της EVM εισάγει και μια νέα πρόκληση: δεν σχεδιάστηκε ώστε να διευκολύνει την ανθρώπινη κατανόηση και τις αυτοματοποιημένες αναλύσεις. Καθώς το EVM bytecode ενός συμβολαίου είναι η μοναδική διαθέσιμη αναπαράσταση εντός του blockchain είναι κρίσιμης σημασίας η δημιουργία αυτοματοποιημένων εργαλείων για την καλύτερη κατανόησή του. Σε αυτή τη διατριβή σχεδιάζουμε και αξιοποιούμε τεχνικές υπερπροσεγγιστικής στατικής ανάλυσης, ώστε να δημιουργήσουμε μια αλυσίδα απομεταγλώττισης που επιτρέπει την αντίστροφη μηχανική και μεταγενέστερες αναλύσεις προγραμμάτων. Η αλυσίδα απομετα-γλώττισης που προτείνουμε αφαιρεί προοδευτικά τα τεχνουργήματα μεταγλώττισης που εισάγονται κατά τη μεταγλώττιση υψηλού επιπέδου πηγαίου κώδικα σε EVM bytecode, ανακτώντας υψηλότερου επιπέδου έννοιες. Οι συνεισφορές της διατριβής χωρίζονται σε δύο μέρη. Το πρώτο μέρος εστιάζει στην ανάκτηση μιας δομημένης ενδιάμεσης αναπαράστασης με συναρτήσεις, μεταβλητές/κατα-χωρητές και επιλυμένες ακμές ροής ελέγχου από το χαμηλού επιπέδου, βασισμένο στη στοίβα, bytecode που στερείται όλων των παραπάνω. Στο δεύτερο μέρος της διατριβής, αξιοποιούμε αυτή την αναπαράσταση για να την εμπλουτίσουμε με πρόσθετη πληροφορία σχετικά με τα αντικείμενα που αποθηκεύονται στις διάφορες δομές τύπου σωρού της EVM. Ένα επαναλαμβανόμενο θέμα των συνεισφορών στο πρώτο μέρος της διατριβής είναι η χρήση παραλλαγών context sensitivity, προσαρμοσμένων στο πεδίο, για τον υπολογισμό του γράφου ροής ελέγχου (CFG) του προγράμματος με ακριβή, πλήρη και κλιμακούμενο τρόπο. Αυτός ο context-sensitive CFG χρησιμοποιείται στη συνέχεια για την αναγνώριση δημόσιων και ιδιωτικών συναρτήσεων στο αδόμητο εισερχόμενο bytecode. Μαζί με άλλες τεχνικές που παρουσιάζονται, όπως η κλωνοποίηση χαμηλού επιπέδου blocks, το εργαλείο ανύψωσής μας αξιολογήθηκε επιτυχώς έναντι εργαλείων αιχμής από την ακαδημαϊκή και τη βιομηχανική κοινότητα. Στο δεύτερο μέρος της διατριβής εστιάζουμε στη μοντελοποίηση των αποθηκών της EVM. Αρχικά επικεντρωνόμαστε στη "μνήμη" (memory), μια παροδική σωρό που χρησιμοποιεί-ται για διασυμβολαιακή επικοινωνία, υπολογισμό κρυπτογραφικών κατακερματισμών και άλλα. Όλες αυτές οι υψηλού επιπέδου έννοιες μεταγλωττίζονται σε εντολές αποθήκευσης και φόρτωσης στη μνήμη, οι οποίες λειτουργούν πάνω σε δείκτες χαμηλού επιπέδου. Σχεδιάζουμε μια ανάλυση που ανακτά πληροφορία υψηλού επιπέδου και καταφέρνουμε να μοντελοποιήσουμε πάνω από το 92% των εντολών αποθήκευσης και φόρτωσης χαμηλού επιπέδου. Η τελευταία μας συνεισφορά εστιάζει στην ανάκτηση δομής στη μόνιμη σωρό (storage) της EVM. Σχεδιάζουμε και υλοποιούμε μια ανάλυση που ανακτά τις αυθαίρετα εμφωλευμένες δομές δεδομένων που εδράζουν στο storage, καταφέρνοντας να ξεπερά-σουμε τo state-of-the-art σε όλους τους άξονες (κλιμάκωση, ακρίβεια και πληρότητα), ενώ συχνά συμπεραίνουμε περισσότερες δομές από εκείνες που προκύπτουν από τα μεταδεδομένα που παράγει ο μεταγλωττιστής. Τέλος, δείχνουμε πώς η μοντελοποίηση της μνήμης και του storage είναι καθοριστική για πολλές μεταγενέστερες αναλύσεις.