Modeling and Verifying Access Control for Ethereum Smart Contracts
Frederik Reiche, Jonas Schiffl, Bernhard Beckert, Robert Heinrich, Ralf Reussner · Repository KITopen (Karlsruhe Institute of Technology) · 2021
Smart contracts are programs on decentralized platforms.They provide services in the form of function calls, which are in principle visible to and callable by everyone on the network.However, smart contracts often contain some functionality intended only for a restricted subset of callers.Such smart contracts require access control.In this work, we develop an approach for modelling access control on the architecture level, using the Palladio tool.From this model, we automatically generate code stubs and source code which enforces access control.Furthermore, we generate a formal specication such that if the implementation adheres to this specication, access control is correct according to the model.We also describe our concrete experience with formal verication of the generated as well as the interactively written specication.Overall, our approach enables dening an access control model on a high level of abstraction, and ensuring its correct implementation.