Combining Model Checking and Testing in a Continuous HW/SW Co-verification Process

2009 ◽  
pp. 121-136 ◽  
Author(s):  
Paula Herber ◽  
Florian Friedemann ◽  
Sabine Glesner
Keyword(s):  
Model Checking ◽  
Verification Process

scholarly journals Model-Checking Speculation-Dependent Security Properties: Abstracting and Reducing Processor Models for Sound and Complete Verification

Electronics ◽  
2019 ◽  
Vol 8 (9) ◽  
pp. 1057
Author(s):  
Gianpiero Cabodi ◽  
Paolo Camurati ◽  
Fabrizio Finocchiaro ◽  
Danilo Vendraminetto
Keyword(s):  
Model Checking ◽  
Formal Verification ◽  
High Performance ◽  
State Of The Art ◽  
Realistic Model ◽  
Bounded Model Checking ◽  
Sensitive Information ◽  
Model Checker ◽  
Verification Process ◽  
Verification Techniques

Spectre and Meltdown attacks in modern microprocessors represent a new class of attacks that have been difficult to deal with. They underline vulnerabilities in hardware design that have been going unnoticed for years. This shows the weakness of the state-of-the-art verification process and design practices. These attacks are OS-independent, and they do not exploit any software vulnerabilities. Moreover, they violate all security assumptions ensured by standard security procedures, (e.g., address space isolation), and, as a result, every security mechanism built upon these guarantees. These vulnerabilities allow the attacker to retrieve leaked data without accessing the secret directly. Indeed, they make use of covert channels, which are mechanisms of hidden communication that convey sensitive information without any visible information flow between the malicious party and the victim. The root cause of this type of side-channel attacks lies within the speculative and out-of-order execution of modern high-performance microarchitectures. Since modern processors are hard to verify with standard formal verification techniques, we present a methodology that shows how to transform a realistic model of a speculative and out-of-order processor into an abstract one. Following related formal verification approaches, we simplify the model under consideration by abstraction and refinement steps. We also present an approach to formally verify the abstract model using a standard model checker. The theoretical flow, reliant on established formal verification results, is introduced and a sketch of proof is provided for soundness and correctness. Finally, we demonstrate the feasibility of our approach, by applying it on a pipelined DLX RISC-inspired processor architecture. We show preliminary experimental results to support our claim, performing Bounded Model-Checking with a state-of-the-art model checker.

Fepchecker: An Automatic Model Checker for Verifying Fairness and Non-Repudiation of Security Protocols in Web Service

2016 ◽  
Vol 26 (04) ◽  
pp. 563-585 ◽  
Author(s):  
Xiaohong Li ◽  
Jiayi Xu ◽  
Guangquan Xu ◽  
Jianye Hao ◽  
Xiaoru Li ◽  
...  
Keyword(s):  
Model Checking ◽  
Web Service ◽  
Current Model ◽  
Model Checker ◽  
Cryptographic Primitives ◽  
Application Range ◽  
Pi Calculus ◽  
Security Properties ◽  
Verification Process ◽  
Critical Model

Ensuring the fairness and non-repudiation in the security exchange protocol of web service is critical. Model checking is often used for automatic verification for the security properties of protocol. However, the current model checker tools cannot support formalizing protocols with cryptographic primitives, specifying properties with linear temporal logic (LTL) and automatically generating resilient intruder model simultaneously and the application range of them is severely limited. To solve this problem, a model checker Fepchecker is proposed to verify the fairness and non-repudiation properties, which are critical features in security exchange protocols. Firstly, applied pi-calculus is extended to specify the protocols, and the LTL assertion is used for precisely describing fairness and non-repudiation. Secondly, an intruder model is applied to construct their behavior sequences automatically and the protocol sessions and message pattern are used to alleviate the states explosion problem. Thirdly, in our model checking algorithm, the fairness and non-repudiation properties are verified based on Labeled Transition System (LTS) semantics model and the MakeOneMove method is used to explore the state space on-the-fly in the verification process. Finally, Fepchecker is applied to verify six representative protocols and the results show that Fepchecker can effectively verify their fairness and non-repudiation properties.

scholarly journals Pemodelan dan Verifikasi Formal Protokol EE-OLSR dengan UPPAAL CORA

2016 ◽  
Vol 10 (1) ◽  
pp. 93
Author(s):  
Rachmat Wahid Saleh Insani ◽  
Reza Pulungan
Keyword(s):  
Model Checking ◽  
Energy Efficient ◽  
Timed Automata ◽  
Packet Transmission ◽  
Model Checker ◽  
Link State ◽  
Internet Users ◽  
Information And Communication ◽  
Fully Automatic ◽  
Verification Process

Information and Communication Technology systems is a most important part of society.  These systems are becoming more and more complex and are massively encroaching on daily life via the Internet and all kinds of embedded systems. Communication protocols are one of the ICT systems used by Internet users. OLSR protocol is a wireless network communication protocol with proactive, and based on link-state algorithm. EE-OLSR protocol is a variant of OLSR that is able to prolong the network lifetime without losses of performance.Protocol verification process generally be done by simulation and testing. However, these processes unable to verify there are no subtle error or design flaw in protocol. Model Checking is an algorithmic method runs in fully automatic to verify a system. UPPAAL is a model checker tool to model, verify, and simulate a system in Timed Automata.UPPAAL CORA is model checker tool to verify EE-OLSR protocol modelled in Linearly Priced Timed Automata, if the protocol satisfy the energy efficient property formulated by formal specification language in Weighted Computation Tree Logic syntax. Model Checking Technique to verify the protocols results in the protocol is satisfy the energy efficient property only when the packet transmission traffic happens.

Model Checking Control Software for Nonlinear Dynamic Systems

2008 ◽  
Author(s):  
James Kapinski ◽  
Alexandre Donze ◽  
Flavio Lerda ◽  
Hitashyam Maka ◽  
Edmund Clarke ◽  
...  
Keyword(s):  
Model Checking ◽  
Dynamic Systems ◽  
Nonlinear Dynamic ◽  
Nonlinear Dynamic Systems ◽  
Control Software

Discovery of a Difluoroglycine Synthesis Method through Quantum Chemical Calculations

2020 ◽  
Author(s):  
Tsuyoshi Mita ◽  
Yu Harabuchi ◽  
Satoshi Maeda
Keyword(s):  
Quantum Chemical Calculations ◽  
Experimental Verification ◽  
Quantum Chemical ◽  
Synthesis Method ◽  
Target Product ◽  
Systematic Exploration ◽  
Hands On ◽  
Retrosynthetic Analysis ◽  
Synthetic Routes ◽  
Verification Process

The systematic exploration of synthetic pathways to afford a desired product through quantum chemical calculations remains a considerable challenge. In 2013, Maeda et al. introduced ‘quantum chemistry aided retrosynthetic analysis’ (QCaRA), which uses quantum chemical calculations to search systematically for decomposition paths of the target product and propose a synthesis method. However, until now, no new reactions suggested by QCaRA have been reported to lead to experimental discoveries. Using a difluoroglycine derivative as a target, this study investigated the ability of QCaRA to suggest various synthetic paths to the target without relying on previous data or the knowledge and experience of chemists. Furthermore, experimental verification of the seemingly most promising path led to the discovery of a synthesis method for the difluoroglycine derivative. The extent of the hands-on expertise of chemists required during the verification process was also evaluated. These insights are expected to advance the applicability of QCaRA to the discovery of viable experimental synthetic routes.

Discovery of a Difluoroglycine Synthesis Method through Quantum Chemical Calculations

2020 ◽  
Author(s):  
Tsuyoshi Mita ◽  
Yu Harabuchi ◽  
Satoshi Maeda
Keyword(s):  
Quantum Chemical Calculations ◽  
Experimental Verification ◽  
Quantum Chemical ◽  
Synthesis Method ◽  
Target Product ◽  
Systematic Exploration ◽  
Hands On ◽  
Retrosynthetic Analysis ◽  
Synthetic Routes ◽  
Verification Process

The systematic exploration of synthetic pathways to afford a desired product through quantum chemical calculations remains a considerable challenge. In 2013, Maeda et al. introduced ‘quantum chemistry aided retrosynthetic analysis’ (QCaRA), which uses quantum chemical calculations to search systematically for decomposition paths of the target product and propose a synthesis method. However, until now, no new reactions suggested by QCaRA have been reported to lead to experimental discoveries. Using a difluoroglycine derivative as a target, this study investigated the ability of QCaRA to suggest various synthetic paths to the target without relying on previous data or the knowledge and experience of chemists. Furthermore, experimental verification of the seemingly most promising path led to the discovery of a synthesis method for the difluoroglycine derivative. The extent of the hands-on expertise of chemists required during the verification process was also evaluated. These insights are expected to advance the applicability of QCaRA to the discovery of viable experimental synthetic routes.

Sign in / Sign up

Export Citation Format

Share Document