Automatic program verification in Dynamic Logic with applications to smart contracts
Resumo
In critical systems, failures or errors can cause catastrophes, such as deaths or considerably losses of money. Model checking provides an automated way to prove the correctness of programs' requirements. It is a convenient technique to use in systems that need reliability. Propositional Dynamic Logic (PDL) is a formal system designed to reason about programs. This work presents a compiler implementation from a subset of the C language and also for the Smacco model, both to the PDL language, and after that to the language of the nuXmv model checker. This implementation is linked with a Blockchain model generation system to model and reason about smart contracts.
Palavras-chave:
Dynamic Logic, Model Checking, Smart Contracts
Referências
Tesnim Abdellatif and Kei-Leo Brousmiche. Formal verification of smart contracts based on users and blockchain behaviors models. 2018 9th IFIP International Conference on New Technologies, Mobility and Security (NTMS), Feb 2018, pp. 1–5.
H. R. Andersen. An introduction to binary decision diagrams. Lecture notes, available online, IT University of Copenhagen, p. 5, 1997.
David M. Beazley. PLY (Python Lex-Yacc). https://www.dabeaz.com/ply/ply.html.
R. Cavada, A. Cimatti, M. Dorigatti, A. Griggio, A. Mariotti, A. Micheli, S. Mover, M. Roveri, and S. Tonetta. The nuxmv symbolic model checker. CAV, ser. Lecture Notes in Computer Science, A. Biere and R. Bloem, Eds., vol. 8559, Springer, 2014,pp. 334–342.
Alessandro Cimatti, Edmund Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pi-store, Marco Roveri, Roberto Sebastiani, and Armando Tacchella. Nusmv 2: An opensource tool for symbolic model checking. Computer Aided Verification, E.Brinksma and K. G. Larsen, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg,2002, pp. 359–364.
Vitor N. Coelho, Thays A. Oliveira, Wellington Tavares, and Igor M. Coelho. Smart accounts for decentralized governance on smart cities (to appear).Smart Cities, 2021.
Bruno Olímpio Costa. Verificação formal de modelos de blockchain. Master’s thesis, Universidade Federal Fluminense, 2019.
S. Gerhart, D. Craigen, and T. Ralston. Case study: Paris metro signaling system. IEEE Software, vol. 11, no. 1, pp. 32–28, 1994.
David Harel, Dexter Kozen, and Jerzy Tiuryn. Dynamic Logic. MIT Press, 2000.
Michael J.Fischer and Richard E.Ladner. Propositional dynamic logic of regular programs. Journal of Computer and System Sciences, 1979.
J. C. Knight. Safety critical systems: challenges and directions. Proceedings of the 24th International Conference on Software Engineering, ACM, 2002, pp. 547–550.
Yubi Lee. flex-bison. https://github.com/eubnara/flex-bison.
Igor Machado. Smacco. https://neo-smacco.readthedocs.io/en/latest/intro.html.
Satoshi Nakamoto. Bitcoin: A peer-to-peer electronic cash system. https://bitcoin.org/bitcoin.pdf, 2009.
C. Sinz, W. Kuchlin, and T. Lumpp. Towards a verification of the rule-based expert system of the ibm sa for os/390 automation manager. In Proceedings Second Asia-Pacific Conference on Quality Software, pages 367–374, 2001.
H. R. Andersen. An introduction to binary decision diagrams. Lecture notes, available online, IT University of Copenhagen, p. 5, 1997.
David M. Beazley. PLY (Python Lex-Yacc). https://www.dabeaz.com/ply/ply.html.
R. Cavada, A. Cimatti, M. Dorigatti, A. Griggio, A. Mariotti, A. Micheli, S. Mover, M. Roveri, and S. Tonetta. The nuxmv symbolic model checker. CAV, ser. Lecture Notes in Computer Science, A. Biere and R. Bloem, Eds., vol. 8559, Springer, 2014,pp. 334–342.
Alessandro Cimatti, Edmund Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pi-store, Marco Roveri, Roberto Sebastiani, and Armando Tacchella. Nusmv 2: An opensource tool for symbolic model checking. Computer Aided Verification, E.Brinksma and K. G. Larsen, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg,2002, pp. 359–364.
Vitor N. Coelho, Thays A. Oliveira, Wellington Tavares, and Igor M. Coelho. Smart accounts for decentralized governance on smart cities (to appear).Smart Cities, 2021.
Bruno Olímpio Costa. Verificação formal de modelos de blockchain. Master’s thesis, Universidade Federal Fluminense, 2019.
S. Gerhart, D. Craigen, and T. Ralston. Case study: Paris metro signaling system. IEEE Software, vol. 11, no. 1, pp. 32–28, 1994.
David Harel, Dexter Kozen, and Jerzy Tiuryn. Dynamic Logic. MIT Press, 2000.
Michael J.Fischer and Richard E.Ladner. Propositional dynamic logic of regular programs. Journal of Computer and System Sciences, 1979.
J. C. Knight. Safety critical systems: challenges and directions. Proceedings of the 24th International Conference on Software Engineering, ACM, 2002, pp. 547–550.
Yubi Lee. flex-bison. https://github.com/eubnara/flex-bison.
Igor Machado. Smacco. https://neo-smacco.readthedocs.io/en/latest/intro.html.
Satoshi Nakamoto. Bitcoin: A peer-to-peer electronic cash system. https://bitcoin.org/bitcoin.pdf, 2009.
C. Sinz, W. Kuchlin, and T. Lumpp. Towards a verification of the rule-based expert system of the ibm sa for os/390 automation manager. In Proceedings Second Asia-Pacific Conference on Quality Software, pages 367–374, 2001.
Publicado
18/07/2021
Como Citar
PATRICK, Allan; COELHO, Igor Machado; LOPES, Bruno.
Automatic program verification in Dynamic Logic with applications to smart contracts. In: WORKSHOP BRASILEIRO DE LÓGICA (WBL), 2. , 2021, Evento Online.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2021
.
p. 1-8.
ISSN 2763-8731.
DOI: https://doi.org/10.5753/wbl.2021.15772.
