HabrFeb 10

Применяем формальные методы к чейнкодам Hyperledger Fabric: кейс BaseToken

Добрый день! Меня зовут Кирилл Зиборов, я представляю отдел безопасности распределенных систем Positive Technologies. В этой статье я продолжу рассказывать о том, как мы используем инструменты формальной верификации для предотвращения уязвимостей в различных компонентах блокчейна. Речь пойдет о верификации смарт-контракта BaseToken в Hyperledger Fabric с помощью метода проверки моделей.

https://habr.com/ru/companies/pt/articles/993688/

#Hypeledger_Fabric #смартконтракты #чейнкод #формальная_верификация_криптовалют #model_checking #tla+ #блокчейн #hlf

Применяем формальные методы к чейнкодам Hyperledger Fabric: кейс BaseToken

Добрый день! Меня зовут Кирилл Зиборов, я представляю отдел безопасности распределенных систем Positive Technologies. В этой статье я продолжу рассказывать о том, как мы используем инструменты...

Хабр
HabrDec 10, 2024

Формальная верификация протокола IBFT: проверяем безопасность византийского консенсуса в блокчейне

Добрый день! Меня зовут Кирилл Зиборов, я представляю отдел безопасности распределенных систем Positive Technologies. В этой статье я продолжу рассказывать о том, как мы используем инструменты формальной верификации для предотвращения уязвимостей в различных компонентах блокчейна. Ранее мы верифицировали смарт-контракты дедуктивным методом . В этот раз речь пойдет о протоколах консенсуса — механизмах принятия узлами новых транзакций в цепочку, а именно об алгоритме Istanbul Byzantine Fault Tolerant и в целом о том, как можно гарантировать корректность подобных алгоритмов с помощью метода проверки моделей.

https://habr.com/ru/companies/pt/articles/864754/

#формальная_верификация #formal_verification #протокол_консенсуса #блокчейн #криптовалюты #tla+ #model_checking #IBFT #bft

Формальная верификация протокола IBFT: проверяем безопасность византийского консенсуса в блокчейне

Добрый день! Меня зовут Кирилл Зиборов, я представляю отдел безопасности распределенных систем Positive Technologies. В этой статье я продолжу рассказывать о том, как мы используем инструменты...

Хабр
nopeSep 8, 2023
Model Checking Linear Logic Specifications
(2003) : Bozzano, Marco Delzanno, Giorg...
DOI: https://doi.org/10.48550/ARXIV.CS/0309003
#model_checking #fixpoint_semantics #logic_programming #bottom_up #LO #linear_logic #my_bibtex
Model Checking Linear Logic Specifications

The overall goal of this paper is to investigate the theoretical foundations of algorithmic verification techniques for first order linear logic specifications. The fragment of linear logic we consider in this paper is based on the linear logic programming language called LO enriched with universally quantified goal formulas. Although LO was originally introduced as a theoretical foundation for extensions of logic programming languages, it can also be viewed as a very general language to specify a wide range of infinite-state concurrent systems. Our approach is based on the relation between backward reachability and provability highlighted in our previous work on propositional LO programs. Following this line of research, we define here a general framework for the bottom-up evaluation of first order linear logic specifications. The evaluation procedure is based on an effective fixpoint operator working on a symbolic representation of infinite collections of first order linear logic formulas. The theory of well quasi-orderings can be used to provide sufficient conditions for the termination of the evaluation of non trivial fragments of first order linear logic.

arXiv.org
nopeAug 13, 2023
Model Checking Linear Logic Specifications
(2003) : Bozzano, Marco Delzanno, Giorg...
DOI: https://doi.org/10.48550/ARXIV.CS/0309003
#bottom_up #fixpoint_semantics #LO #logic_programming #linear_logic #model_checking #my_bibtex
Model Checking Linear Logic Specifications

The overall goal of this paper is to investigate the theoretical foundations of algorithmic verification techniques for first order linear logic specifications. The fragment of linear logic we consider in this paper is based on the linear logic programming language called LO enriched with universally quantified goal formulas. Although LO was originally introduced as a theoretical foundation for extensions of logic programming languages, it can also be viewed as a very general language to specify a wide range of infinite-state concurrent systems. Our approach is based on the relation between backward reachability and provability highlighted in our previous work on propositional LO programs. Following this line of research, we define here a general framework for the bottom-up evaluation of first order linear logic specifications. The evaluation procedure is based on an effective fixpoint operator working on a symbolic representation of infinite collections of first order linear logic formulas. The theory of well quasi-orderings can be used to provide sufficient conditions for the termination of the evaluation of non trivial fragments of first order linear logic.

arXiv.org
nopeMay 18, 2023
Model Checking
(2001) : Merz, Stephan
DOI: https://doi.org/10.1007/3-540-45510-8_1
#temporal_logic #reactive_systems #transition_system #model_checking #needham_schroeder #my_bibtex
nopeJan 14, 2023
Slicing Agent Programs for More Efficient Verification
(2019) : Michael Winikoff and Louise Dennis and Michael Fisher
DOI: https://doi.org/10.1007/978-3-030-25693-7_8
#BDI #MAS #bounded_model_checking #formal_verification #gwendolen #model_checking #
#my_bibtex
nopeSep 19, 2022
Model Checking Linear Logic Specifications
(2003) : Marco Bozzano and Giorgio Delzanno and Maurizio Martelli
DOI: https://doi.org/10.48550/ARXIV.CS/0309003
#LO #bottom_up #fixpoint_semantics #linear_logic #logic_programming #model_checking
#my_bibtex
Model Checking Linear Logic Specifications

The overall goal of this paper is to investigate the theoretical foundations of algorithmic verification techniques for first order linear logic specifications. The fragment of linear logic we consider in this paper is based on the linear logic programming language called LO enriched with universally quantified goal formulas. Although LO was originally introduced as a theoretical foundation for extensions of logic programming languages, it can also be viewed as a very general language to specify a wide range of infinite-state concurrent systems. Our approach is based on the relation between backward reachability and provability highlighted in our previous work on propositional LO programs. Following this line of research, we define here a general framework for the bottom-up evaluation of first order linear logic specifications. The evaluation procedure is based on an effective fixpoint operator working on a symbolic representation of infinite collections of first order linear logic formulas. The theory of well quasi-orderings can be used to provide sufficient conditions for the termination of the evaluation of non trivial fragments of first order linear logic.

arXiv.org
nopeAug 10, 2022
Verifying Social Expectations By Model Checking Truncated Paths
(2011) : Cranefield, Stephen and Winikoff, Michael
DOI: https://doi.org/10.1093/logcom/exq055
#LTL #MAS #algorithm #expectation #institution #logic #model_checking #semantics #social #ve
#my_bibtex
Verifying social expectations by model checking truncated paths

Abstract. One approach to moderating the expected behaviour of agents in open societies is the use of explicit languages for defining norms, conditional commitm

OUP Academic
nopeJul 28, 2022
Symbolic model checking using SAT procedures instead of BDDs
(1999) : A. Biere and A. Cimatti and E.M. Clarke and M. Fujita and Y. Zhu
DOI: https://doi.org/10.1109/dac.1999.781333
#FSMs #SAT #bounded_model_checking #model_checking
#my_bibtex
Symbolic model checking using SAT procedures instead of BDDs

In this paper, we study the application of propositional decision procedures in hardware verification. In particular, we apply bounded model checking to equivalence and invariant checking. We present several optimizations that reduce the size of generated propositional formulas. In many instances, our SAT-based approach can significantly outperform BDD-based approaches. We observe that SAT-based techniques are particularly efficient in detecting errors in both combinational and sequential designs.

nopeJul 27, 2022
Symbolic Model Checking without BDDs
(1999) : Armin Biere and Alessandro Cimatti and Edmund Clarke and Yunshan Zhu
DOI: https://doi.org/10.1007/3-540-49059-0_14
#transition_system #SAT #bounded_model_checking #model_checking
#my_bibtex