Since its introduction in 1999, bounded model checking (BMC) has quickly become a serious and indispensable tool for the formal verification of hardware designs and, more recently, software. By leveraging propositional satisfiability (SAT) solvers, BMC overcomes some of the shortcomings of more conventional model checking methods. In model checking we automatically verify whether a state transition system (STS) describing a design has some property, commonly expressed in linear temporal logic (LTL). BMC is the restriction to only checking the looping and non-looping runs of the system that have bounded descriptions. The conventional BMC approach is to translate the STS runs and LTL formulae into propositional logic and then conjunctive normal form (CNF). This CNF expression is then checked by a SAT solver. In this thesis we study the effect on the performance of BMC of changing the translation to propositional logic. One novelty is to use a normal form for LTL which originates in resolution theorem provers. We introduce the normal form conversion early on in the encoding process and examine the simplifications that it brings to the generation of propositional logic. We further enhance the encoding by specialising the normal form to take advantage of the types of runs peculiar to BMC. We also improve the conversion from propositional logic to CNF. We investigate the behaviour of the new encodings by a series of detailed experimental comparisons using both hand-crafted and industrial benchmarks from a variety of sources. These reveal that the new normal form based encodings can reduce the solving time by a half in most cases, and up to an order of magnitude in some cases, the size of the improvement corresponding to the complexity of the LTL expression. We also compare our method to the popular automata-based methods for model checking and BMC.

Uma importante etapa do desenvolvimento de software é o de levantamento e análise dos requisitos. Porém, durante esta etapa podem ocorrer inconsistências que prejudicarão o andamento do projeto. Além disso, após finalizada a especificação, o cliente pode querer acrescentar ou modificar as funcionalidades do sistema. Tudo isso requer que a especificação do software seja revista, mas isso é altamente custoso, tornando necessário um processo automatizado para simplificar tal revisão. Para lidar com este problema, uma das abordagens utilizadas tem sido o processo de Revisão de Crenças, juntamente com o processo de Verificação de Modelos. O objetivo deste trabalho é utilizar o processo de revisão de crenças e verificação de modelos para avaliar especificações de um projeto procurando inconsistências, utilizando o fragmento universal da Computation Tree Logic (CTL), conhecido como ACTL, e revisá-las gerando sugestões de mudanças na especificação. A nossa proposta é traduzir para lógica clássica tanto o modelo (especificação do software) quanto a propriedade a ser revisada, e então aplicar um resolvedor SAT para verificar a satisfazibilidade da fórmula gerada. A partir da resposta do resolvedor SAT, iremos gerar sugestões válidas de mudanças para a especificação, fazendo o processo de tradução reversa da lógica clássica para o modelo original. / The objective of this work is to join the proccess of belief revision and model checking to evaluate project specifications looking for inconsistences, using the universal fragment of Computation Tree Logic (CTL), known as ACTL, and revise them generating changes suggestions in the specification. Our approach will translate the model (software specification) and the property to be revised to classical logic. Then we will apply a SAT solver to verify the generated formulas satsifability. From the SAT solver answer, we will create changes valid suggestions to the specification making the translation back from classical logic to the original model. To generate the changes suggestions, we proposed a framework based on heuristics where different approaches and decisions can be implemented, aiming a better application for each project scope. We implemented a basic heuristic as an example and used it to test the implementation to analise the proposed algorithm

Submitted by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2017-02-07T17:47:31Z No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Dissertação - Mário A. P. Garcia.pdf: 1777955 bytes, checksum: bbc5f97c856505f518492e5c8ec65c28 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2017-02-07T17:47:47Z (GMT) No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Dissertação - Mário A. P. Garcia.pdf: 1777955 bytes, checksum: bbc5f97c856505f518492e5c8ec65c28 (MD5) / Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2017-02-07T17:48:08Z (GMT) No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Dissertação - Mário A. P. Garcia.pdf: 1777955 bytes, checksum: bbc5f97c856505f518492e5c8ec65c28 (MD5) / Made available in DSpace on 2017-02-07T17:48:08Z (GMT). No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Dissertação - Mário A. P. Garcia.pdf: 1777955 bytes, checksum: bbc5f97c856505f518492e5c8ec65c28 (MD5) Previous issue date: 2016-09-13 / CAPES - Coordenação de Aperfeiçoamento de Pessoal de Nível Superior / The software development for embedded systems is getting faster and faster, which generally incurs an increase in the associated complexity. As a consequence, consumer electronics companies usually invest a lot of resources in fast and automatic verification mechanisms, in order to create robust systems and reduce product recall rates. In addition, further development-time reduction and system robustness can be achieved through cross-platform frameworks, such as Qt, which favor the reliable port of software stacks to different devices. Based on that, the present work proposes a simplified version of the Qt framework, which is integrated into a checker based on satisfiability modulo theories (SMT), name as the efficient SMT-based bounded model checker (ESBMC++), for verifying actual Qt-based applications, and presents a success rate of 89%, for the developed benchmark suite. We also evaluate our simplified version of the Qt framework using other state-of-the-art verifiers for C++ programs and an evaluation about their level of compliance. It is worth mentioning that the proposed methodology is the first one to formally verify Qt-based applications, which has the potential to devise new directions for software verification of portable code. / O desenvolvimento de software para sistemas embarcados tem crescido rapidamente, o que na maioria das vezes acarreta em um aumento da complexidade associada a esse tipo de projeto. Como consequência, as empresas de eletrônica de consumo costumam investir recursos em mecanismos de verificação rápida e automática, com o intuito de desenvolver sistemas robustos e assim reduzir as taxas de recall de produtos. Além disso, a redução no tempo de desenvolvimento e na robustez dos sistemas desenvolvidos podem ser alcançados através de frameworks multi-plataformas, tais como Qt, que oferece um conjunto de bibliotecas (gráficas) confiáveis para vários dispositivos embarcados. Desta forma, este trabalho propõe uma versão simplificada do framework Qt que integrado a um verificador baseado nas teorias do módulo da satisfatibilidade, denominado Efficient SMT-Based Bounded Model Checker (ESBMC++), verifica aplicações reais que ultilizam o Qt, apresentando uma taxa de sucesso de 89%, para os benchmarks desenvolvidos. Com a versão simplificada do framework Qt proposto, também foi feita uma avaliação ultilizando outros verificadores que se encontram no estado da arte para verificação de programas em C++ e uma avalição a cerca de seu nível de conformidade. Dessa maneira, a metodologia proposta se afirma como a primeira a verificar formalmente aplicações baseadas no framework Qt, além de possuir um potencial para desenvolver novas frentes para a verificação de código portátil.

Uma importante etapa do desenvolvimento de software é o de levantamento e análise dos requisitos. Porém, durante esta etapa podem ocorrer inconsistências que prejudicarão o andamento do projeto. Além disso, após finalizada a especificação, o cliente pode querer acrescentar ou modificar as funcionalidades do sistema. Tudo isso requer que a especificação do software seja revista, mas isso é altamente custoso, tornando necessário um processo automatizado para simplificar tal revisão. Para lidar com este problema, uma das abordagens utilizadas tem sido o processo de Revisão de Crenças, juntamente com o processo de Verificação de Modelos. O objetivo deste trabalho é utilizar o processo de revisão de crenças e verificação de modelos para avaliar especificações de um projeto procurando inconsistências, utilizando o fragmento universal da Computation Tree Logic (CTL), conhecido como ACTL, e revisá-las gerando sugestões de mudanças na especificação. A nossa proposta é traduzir para lógica clássica tanto o modelo (especificação do software) quanto a propriedade a ser revisada, e então aplicar um resolvedor SAT para verificar a satisfazibilidade da fórmula gerada. A partir da resposta do resolvedor SAT, iremos gerar sugestões válidas de mudanças para a especificação, fazendo o processo de tradução reversa da lógica clássica para o modelo original. / The objective of this work is to join the proccess of belief revision and model checking to evaluate project specifications looking for inconsistences, using the universal fragment of Computation Tree Logic (CTL), known as ACTL, and revise them generating changes suggestions in the specification. Our approach will translate the model (software specification) and the property to be revised to classical logic. Then we will apply a SAT solver to verify the generated formulas satsifability. From the SAT solver answer, we will create changes valid suggestions to the specification making the translation back from classical logic to the original model. To generate the changes suggestions, we proposed a framework based on heuristics where different approaches and decisions can be implemented, aiming a better application for each project scope. We implemented a basic heuristic as an example and used it to test the implementation to analise the proposed algorithm

Runtime Verification (RV) is usually considered as a lightweight automatic verification technique for the dynamic analysis of systems, where a monitor observes executions produced by a system and analyzes its executions against a formal specification. If the monitor were synthesized, in addition to the monitoring specification, also from extra assumptions on the system behavior (typically described by a model as transition systems), then it may output more precise verdicts or even be predictive, meanwhile it may no longer be lightweight, since monitoring under assumptions has the same computation complexity with model checking. When suitable assumptions come into play, the monitor may also support partial observability, where non-observable variables in the specification can be inferred from observables, either present or historical ones. Furthermore, the monitors are resettable, i.e. being able to evaluate the specification at non-initial time of the executions while keeping memories of the input history. This helps in breaking the monotonicity of monitors, which, after reaching conclusive verdicts, can still change its future outputs by resetting its reference time. The combination of the above three characteristics (assumptions, partial observability and resets) in the monitor synthesis is called the Assumption-Based Runtime Verification, or ABRV. In this thesis, we give the formalism of the ABRV approach and a group of monitoring algorithms based on specifications expressed in Linear Temporal Logic with both future and past operators, involving Boolean and possibly other types of variables. When all involved variables have finite domain, the monitors can be synthesized as finite-state machines implemented by Binary Decision Diagrams. With infinite-domain variables, the infinite-state monitors are based on satisfiability modulo theories, first-order quantifier elimination and various model checking techniques. In particular, Bounded Model Checking is modified to do its work incrementally for efficiently obtaining inconclusive verdicts, before IC3-based model checkers get involved. All the monitoring algorithms in this thesis are implemented in a tool called NuRV. NuRV support online and offline monitoring, and can also generate standalone monitor code in various programming languages. In particular, monitors can be synthesized as SMV models, whose behavior correctness and some other properties can be further verified by model checking.

The translation of binary code to higher-level models has wide applications, including decompilation, binary analysis, and binary rewriting. This calls for high reliability of the underlying trusted computing base (TCB) of the translation methodology. A key challenge is to reduce the TCB by validating its soundness. Both the definition of soundness and the validation method heavily depend on the context: what is in the TCB and how to prove it. This dissertation presents three research contributions. The first two contributions include reducing the TCB in binary verification, and the last contribution includes a binary verification process that leverages a reduced TCB. The first contribution targets the validation of OCaml-to-PVS translation -- commonly used to translate instruction-set-architecture (ISA) specifications to PVS -- where the destination language is non-executable. We present a methodology called OPEV to validate the translation between OCaml and PVS, supporting non-executable semantics. The validation includes generating large-scale tests for OCaml implementations, generating test lemmas for PVS, and generating proofs that automatically discharge these lemmas. OPEV incorporates an intermediate type system that captures a large subset of OCaml types, employing a variety of rules to generate test cases for each type. To prove the PVS lemmas, we develop automatic proof strategies and discharge the test lemmas using PVS Proof-Lite, a powerful proof scripting utility of the PVS verification system. We demonstrate our approach in two case studies that include 259 functions selected from the Sail and Lem libraries. For each function, we generate thousands of test lemmas, all of which are automatically discharged. The dissertation's second contribution targets the soundness validation of a disassembly process where the source language does not have well-defined semantics. Disassembly is a crucial step in binary security, reverse engineering, and binary verification. Various studies in these fields use disassembly tools and hypothesize that the reconstructed disassembly is correct. However, disassembly is an undecidable problem. State-of-the-art disassemblers suffer from issues ranging from incorrectly recovered instructions to incorrectly assessing which addresses belong to instructions and which to data. We present DSV, a systematic and automated approach to validate whether the output of a disassembler is sound with respect to the input binary. No source code, debugging information, or annotations are required. DSV defines soundness using a transition relation defined over concrete machine states: a binary is sound if, for all addresses in the binary that can be reached from the binary's entry point, the bytes of the (disassembled) instruction located at an address are the same as the actual bytes read from the binary. Since computing this transition relation is undecidable, DSV uses over-approximation by preventing false positives (i.e., the existence of an incorrectly disassembled reachable instruction but deemed unreachable) and allowing, but minimizing, false negatives. We apply DSV to 102 binaries of GNU Coreutils with eight different state-of-the-art disassemblers from academia and industry. DSV is able to find soundness issues in the output of all disassemblers. The dissertation's third contribution is WinCheck: a concolic model checker that detects memory-related properties of closed-source binaries. Bugs related to memory accesses are still a major issue for security vulnerabilities. Even a single buffer overflow or use-after-free in a large program may be the cause of a software crash, a data leak, or a hijacking of the control flow. Typical static formal verification tools aim to detect these issues at the source code level. WinCheck is a model-checker that is directly applicable to closed-source and stripped Windows executables. A key characteristic of WinCheck is that it performs its execution as symbolically as possible while leaving any information related to pointers concrete. This produces a model checker tailored to pointer-related properties, such as buffer overflows, use-after-free, null-pointer dereferences, and reading from uninitialized memory. The technique thus provides a novel trade-off between ease of use, accuracy, applicability, and scalability. We apply WinCheck to ten closed-source binaries available in a Windows 10 distribution, as well as the Windows version of the entire Coreutils library. We conclude that the approach taken is precise -- provides only a few false negatives -- but may not explore the entire state space due to unresolved indirect jumps. / Doctor of Philosophy / Binary verification is a process that verifies a class of properties, usually security-related properties, on binary files, and does not need access to source code. Since a binary file is composed of byte sequences and is not human-readable, in the binary verification process, a number of assumptions are usually made. The assumptions often involve the error-free nature of a set of subsystems used in the verification process and constitute the verification process's trusted computing base (or TCB). The reliability of the verification process therefore depends on how reliable the TCB is. The dissertation presents three research contributions in this regard. The first two contributions include reducing the TCB in binary verification, and the last contribution includes a binary verification process that leverages a reduced TCB. The dissertation's first contribution presents a validation on OCaml-to-PVS translations -- commonly used to translate a computer architecture's instruction specifications to PVS, a language that allows mathematical specifications. To build up a reliable semantical model of assembly instructions, which is assumed to be in the TCB, it is necessary to validate the translation. The dissertation's second contribution validates the soundness of the disassembly process, which translates a binary file to corresponding assembly instructions. Since the disassembly process is generally assumed to be trustworthy in many binary verification works, the TCB of binary verification could be reduced by validating the soundness of the disassembly process. With the reduced TCB, the dissertation introduces WinCheck, the dissertation's third and final contribution: a concolic model checker that validates pointer-related properties of closed-source Windows binaries. The pointer-related properties include absence of buffer overflow, absence of use-after-free, and absence of null-pointer dereference.

With the advances in VLSI and System-On-Chip (SOC) technology, the complexity of hardware systems has increased manifold. Today, 70% of the design cost is spent in verifying these intricate systems. The two most widely used formal methods for design verification are Equivalence Checking and Model Checking. Equivalence Checking requires that the implementation circuit should be exactly equivalent to the specification circuit (golden model). In other words, for each possible input pattern, the implementation circuit should yield the same outputs as the specification circuit. Model checking, on the other hand, checks to see if the design holds certain properties, which in turn are indispensable for the proper functionality of the design. Complexities in both Equivalence Checking and Model Checking are exponential to the circuit size. In this thesis, we firstly propose a novel technique to improve SAT-based Combinational Equivalence Checking (CEC) and Bounded Model Checking (BMC). The idea is to perform a low-cost preprocessing that will statically induce global signal relationships into the original CNF formula of the circuit under verification and hence reduce the complexity of the SAT instance. This efficient and effective preprocessing quickly builds up the implication graph for the circuit under verification, yielding a large set of logic implications composed of direct, indirect and extended backward implications. These two-node implications (spanning time-frame boundaries) are converted into two-literal clauses, and added to the original CNF database. The added clauses constrain the search space of the SAT-solver engine, and provide correlation among the different variables, which enhances the Boolean Constraint Propagation (BCP). Experimental results on large and difficult ISCAS'85, ISCAS'89 (full scan) and ITC'99 (full scan) CEC instances and ISCAS'89 BMC instances show that our approach is independent of the state-of-the-art SAT-solver used, and that the added clauses help to achieve more than an order of magnitude speedup over the conventional approach. Also, comparison with Hyper-Resolution [Bacchus 03] suggests that our technique is much more powerful, yielding non-trivial clauses that significantly simplify the SAT instance complexity. Secondly, we propose a novel global learning technique that helps to identify highly non-trivial relationships among signals in the circuit netlist, thereby boosting the power of the existing implication engine. We call this new class of implications as 'extended forward implications', and show its effectiveness through additional untestable faults they help to identify. Thirdly, we propose a suite of lemmas and theorems to formalize global learning. We show through implementation that these theorems help to significantly simplify a generic CNF formula (from Formal Verification, Artificial Intelligence etc.) by identifying the necessary assignments, equivalent signals, complementary signals and other non-trivial implication relationships among its variables. We further illustrate through experimental results that the CNF formula simplification obtained using our tool outshines the simplification obtained using other preprocessors. / Master of Science

In the first half of this thesis, a novel approach for k-induction bounded model checking using signal domain constraints and property partitioning for proving unreachability of branches in Verilog RTL code is presented. To do this, it approach uses program slicing with respect to the variables of the property under test to generate small-sized SMT formulas that describe the change of variable values between consecutive cycles. Variable substitution is then used on these variables to generate the formula for the subsequent cycles without traversing the abstract syntax tree of the entire design. To reduce the approximation on the induction step, an addition of signal domain constraints is proposed. Moreover, we present the technique for splitting up the property in question to get a better model of the system. The later half of the thesis is concerned with presenting a technique for doing sequential vector compaction on test set generated during simulation based ATPG. Starting with a compaction framework for storing metadata and about the test vectors during generation, this work presented to methods for findind the solution of this compaction problem. The first of these two methods generate the optimum solution by converting the problem appropriate for an optimization solver. The latter method utilizes a heuristics based approach for solving the same problem which generates a comparable but sub-optimal solution while having magnitudes better time and computational efficiency. / Master of Science / Electronic circuits can be described with languages known a hardware description languages like Verilog. The first part of this thesis is concerned about automatically proving if parts of this code is actually useful or reachable when implemented on and actual circuit. The thesis builds up on a method known as bounded model checking which can automatically prove if a property holds or not for a given system. The key insight is obtained from the fact that various memory elements in a circuit is allowed to be only in a certain range of values during the design process. The later half of this thesis is gear towards generating minimum sized inputs values to a circuit required for testing it. This work uses large sized input values to circuits generated by a previously published tool and proposes a way to make them smaller. This can reduce cost immensely for testing circuits in the industry where even the smallest increase in testing time increases cost of development immensely. There are two such approaches presented, one of which gives the optimum result but takes a long time to run for larger circuits, while the other gives comparable but sub-optimal result in a much more time efficient manner.

Problems in formal verification are often stated in terms of finite automata and extensions thereof. In this thesis we investigate several such algorithmic problems. In the first part of the thesis we develop a theory of completeness thresholds in Bounded Model Checking. A completeness threshold for a given model M and a specification φ is a bound k such that, if no counterexample to φ of length k or less can be found in M, then M in fact satisfies φ. We settle a problem of Kroening et al. [KOS⁺11] in the affirmative, by showing that the linearity problem for both regular and ω-regular specifications (provided as finite automata and Buchi automata respectively) is PSPACE-complete. Moreover, we establish the following dichotomies: for regular specifications, completeness thresholds are either linear or exponential, whereas for ω-regular specifications, completeness thresholds are either linear or at least quadratic in the recurrence diameter of the model under consideration. Given a formula in a temporal logic such as LTL or MTL, a fundamental problem underpinning automata-based model checking is the complexity of evaluating the formula on a given finite word. For LTL, the complexity of this task was recently shown to be in NC [KF09]. In the second part of the thesis we present an NC algorithm for MTL, a quantitative (or metric) extension of LTL, and give an AC¹ algorithm for UTL, the unary fragment of LTL. We then establish a connection between LTL path checking and planar circuits which, among others, implies that the complexity of LTL path checking depends on the Boolean connectives allowed: adding Boolean exclusive or yields a temporal logic with P-complete path-checking problem. In the third part of the thesis we study the decidability of the reachability problem for parametric timed automata. The problem was introduced over 20 years ago by Alur, Henzinger, and Vardi [AHV93]. It is known that for three or more parametric clocks the problem is undecidable. We translate the problem to reachability questions in certain extensions of parametric one-counter machines. By further reducing to satisfiability in Presburger arithmetic with divisibility, we obtain decidability results for several classes of parametric one-counter machines. As a corollary, we show that, in the case of a single parametric clock (with arbitrarily many nonparametric clocks) the reachability problem is NEXP-complete, improving the nonelementary decision procedure of Alur et al. The case of two parametric clocks is open. Here, we show that the reachability is decidable in this case of automata with a single parameter.

Stateflowmodels are used for describing logic and implementing state machines in modern safety-critical software. However, the complete Stateflowmodelling language is hard to formally define, therefore a subset relevant for industrial models has been developed in previous works. Proving that the execution of Stateflow models satisfies certain safety properties is intractable in general. However, bounded model checking (BMC) can be used to either prove that safety properties are satisfied up to a bounded execution depth, commonly referred to as the reachability diameter, or find a concrete counterexample. One particular safety property of interest is an invariant property. This thesis project contributes with the following. A bounded model checking tool based on symbolic execution has been developed and is called Stateflow Model Verification Tool (SMVT). This tool has been tested on synthetic models and industrial models. The performance of Stateflow Model Verification Tool (SMVT) has been measured, but not compared against the Simulink DesignVerifier (SLDV) due to licensing issues. The study has shown that many industrial models share a similar model structure. Furthermore, it has been shown that SMVT can perform well for several models. / Stateflow-modeller används för att beskriva logik and implementation av tillståndsmaskiner i modern säkerhetskritisk mjukvara. Det kompletta Stateflowspråket är väldigt komplext, och därför har forskare tidigare definierat en begränsad version av språket relevant för industriella modeller. Bevisning att exekvering av Stateflow-modeller måste uppfylla säkerhetsegenskaper, är svårlösligt rent generellt. Begränsad modellprovning kan användas antingen för att bevisa att säkerhetsegenskaper uppfylls till ett begränsat exekveringsdjup, eller för att hitta ett motexempel. En väldigt viktig säkerhetsegenskap kallas för invariant. Detta examensarbete bidrar med följande. En begränsad modellprövare baserad på symbolisk exekvering har utvecklats och kallas för SMVT. Detta verktyg har blivit testat på syntetiska modeller samt industriella modeller. Prestandan har blivit mätt, men på grund av Simulink Design Verifier (SLDV) licens har ingen jämförelse kunnat göras. Studien har visat att många industriella modeller delar samma modellstruktur. Vidare har det utvecklade verktyget SMVT visats prestera väl för flertalet modeller.