Abstract
Ensuring correctness of smart contracts is paramount to ensuring trust in blockchain-based systems. This paper studies the safety and security of smart contracts in the Azure Blockchain Workbench, an enterprise Blockchain-as-a-Service offering from Microsoft. In particular, we formalize semantic conformance of smart contracts against a state machine workflow with access-control policy and propose an approach to reducing semantic conformance checking to safety verification using program instrumentation. We develop a new Solidity program verifier VeriSol that is based on translation to Boogie, and have applied it to analyze all application contracts shipped with the Azure Blockchain Workbench and found previously unknown bugs in these published smart contracts. After fixing these bugs, VeriSol was able to successfully perform full verification for all of these contracts.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
- 2.
The details can be found on the associated web page: https://github.com/Azure-Samples/blockchain/tree/master/blockchain-workbench/application-and-smart-contract-samples/hello-blockchain.
- 3.
We omit several aspects of the language such as arrays and mappings due to space limit. More details can be found in the extended version of this paper [30].
- 4.
We assume that the hash function is collision-free. In our implementation, we enforce this by keeping a mapping from each string constant to a counter.
References
Explaining the DAO exploit for beginners in solidity (2016). https://medium.com/@MyPaoG/explaining-the-dao-exploit-for-beginners-in-solidity-80ee84f0d470
Solidity: Function modifiers (2016). https://solidity.readthedocs.io/en/v0.4.24/structure-of-a-contract.html#function-modifiers
Forecast: Blockchain business value, worldwide, 2017–2030 (2017). https://www.gartner.com/en/documents/3627117
Microsoft azure blockchain (2017). https://azure.microsoft.com/en-us/solutions/blockchain/
Parity: The bug that put \$169m of ethereum on ice? Yeah, it was on the todo list for months (2017). https://www.theregister.co.uk/2017/11/16/parity_flaw_not_fixed
Applications and smart contract samples for workbench (2018). https://github.com/Azure-Samples/blockchain/tree/master/blockchain-workbench/application-and-smart-contract-samples
Asset transfer sample for azure blockchain workbench (2018). https://github.com/Azure-Samples/blockchain/tree/master/blockchain-workbench/application-and-smart-contract-samples/asset-transfer
Azure blockchain content and samples (2018). https://github.com/Azure-Samples/blockchain
Azure blockchain workbench (2018). https://azure.microsoft.com/en-us/features/blockchain-workbench/
Manticore (2018). https://github.com/trailofbits/manticore
Mythril classic: Security analysis tool for ethereum smart contracts (2018). https://github.com/ConsenSys/mythril-classic
Slither, the solidity source analyzer (2018). https://github.com/trailofbits/slither
Verisol: A formal verifier and analysis tool for solidity smart contracts (2018). https://github.com/Microsoft/verisol
Atzei, N., Bartoletti, M., Cimoli, T.: A survey of attacks on ethereum smart contracts (SoK). In: Maffei, M., Ryan, M. (eds.) POST 2017. LNCS, vol. 10204, pp. 164–186. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54455-6_8
Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364–387. Springer, Heidelberg (2006). https://doi.org/10.1007/11804192_17
Bhargavan, K., et al.: Formal verification of smart contracts: short paper. In Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security, PLAS@CCS 2016, Vienna, Austria, 24 October 2016, pp. 91–96 (2016)
Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for ESC/Java. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 500–517. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45251-6_29
Grech, N., Kong, M., Jurisevic, A., Brent, L., Scholz, B., Smaragdakis, Y.: MadMax: surviving out-of-gas conditions in ethereum smart contracts. PACMPL 2(OOPSLA), 116:1–116:27 (2018)
Grossman, S., et al.: Online detection of effectively callback free objects with applications to smart contracts. PACMPL 2(POPL), 48:1–48:28 (2018)
Hildenbrandt, E., et al.: KEVM: a complete formal semantics of the ethereum virtual machine. In 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, United Kingdom, 9–12 July 2018, pp. 204–217 (2018)
Kalra, S., Goel, S., Dhawan, M., Sharma, S.: ZEUS: analyzing safety of smart contracts. In: 25th Annual Network and Distributed System Security Symposium, NDSS 2018, San Diego, California, USA, 18–21 February 2018 (2018)
Lahiri, S.K., Qadeer, S.: Complexity and algorithms for monomial and clausal predicate abstraction. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 214–229. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02959-2_18
Lahiri, S.K., Qadeer, S., Galeotti, J.P., Voung, J.W., Wies, T.: Intra-module inference. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 493–508. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02658-4_37
Lal, A., Qadeer, S., Lahiri, S.K.: A solver for reachability modulo theories. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 427–443. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31424-7_32
Rustan, K., Leino, M.: Efficient weakest preconditions. Inf. Process. Lett. 93(6), 281–288 (2005)
Luu, L., Chu, D.H., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In: Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, Vienna, Austria, 24–28 October 2016, pp. 254–269 (2016)
Mavridou, A., Laszka, A.: Tool demonstration: Fsolidm for designing secure ethereum smart contracts. In: Principles of Security and Trust - 7th International Conference, POST 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, 14–20 April 2018, Proceedings, pp. 270–277 (2018)
Nikolic, I., Kolluri, A., Sergey, I., Saxena, P., Hobor, A.: Finding the greedy, prodigal, and suicidal contracts at scale. In: Proceedings of the 34th Annual Computer Security Applications Conference, ACSAC 2018, San Juan, PR, USA, 03–07 December 2018, pp. 653–663 (2018)
Tsankov, P., et al.: Securify: practical security analysis of smart contracts. In: Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS 2018, Toronto, ON, Canada, 15–19 October 2018, pp. 67–82 (2018)
Wang, Y., et al.: Formal specification and verification of smart contracts in azure blockchain (2018). https://arxiv.org/abs/1812.08829/
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Wang, Y. et al. (2020). Formal Verification of Workflow Policies for Smart Contracts in Azure Blockchain. In: Chakraborty, S., Navas, J. (eds) Verified Software. Theories, Tools, and Experiments. VSTTE 2019. Lecture Notes in Computer Science(), vol 12031. Springer, Cham. https://doi.org/10.1007/978-3-030-41600-3_7
Download citation
DOI: https://doi.org/10.1007/978-3-030-41600-3_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-41599-0
Online ISBN: 978-3-030-41600-3
eBook Packages: Computer ScienceComputer Science (R0)