No description available.

No description available.

Doctor of Philosophy / Department of Computing and Information Sciences / John M. Hatcliff / High-integrity applications are safety- and security-critical applications developed for a variety of critical tasks. The correctness of these applications must be thoroughly tested or formally verified to ensure their reliability and robustness. The major properties to be verified for the correctness of applications include: (1) functional properties, capturing the expected behaviors of a software, (2) dataflow property, tracking data dependency and preventing secret data from leaking to the public, and (3) robustness property, the ability of a program to deal with errors during execution. This dissertation presents and explores formal verification and proof technique, a promising technique using rigorous mathematical methods, to verify critical applications from the above three aspects. Our research is carried out in the context of SPARK, a programming language designed for development of safety- and security-critical applications. First, we have formalized in the Coq proof assistant the dynamic semantics for a significant subset of the SPARK 2014 language, which includes run-time checks as an integral part of the language, as any formal methods for program specification and verification depend on the unambiguous semantics of the language. Second, we have formally defined and proved the correctness of run-time checks generation and optimization based on SPARK reference semantics, and have built the certifying tools within the mechanized proof infrastructure to certify the run-time checks inserted by the GNAT compiler frontend to guarantee the absence of run-time errors. Third, we have proposed a language-based information security policy framework and the associated enforcement algorithm, which is proved to be sound with respect to the formalized program semantics. We have shown how the policy framework can be integrated into SPARK 2014 for more advanced information security analysis.

There are a number of techniques for automatic bug detection, most of them have a high false positive rate when used in practice. This work proposes an approach, named Strip-Miner, that combines simple dependency analysis of code with a data mining technique "frequent itemset mining" to reduce the false positive rate. We adopt a two phase approach 1) finding the potential bugs and 2) filtering the false positive ones. In the first phase we extract code elements and dependencies among them using static analysis and frequent itemset mining to find programming patterns where a deviation from these patterns is considered as a potential bug. In the second phase, we use the extracted dependencies to build dependency chains between program elements in a programming pattern and a lack of such a chain potentially makes a bug false positive. Our evaluation on a set of 7 benchmarks consisting of large software code including OpenSSL, PostgreSQL, Git, FFMPEG, SQLite, Binutils and Putty shows that combining simple de- pendency analysis with pattern mining can significantly decrease the number of generated bugs. Using our approach we are able to reduce the number of generated bugs by up to 99.9% with a false positive rate of 65.19% and true positive rate of 34.18% on average as compared to an earlier frequent itemset mining based approach "PR-Miner". / Master of Science / Every software code has bugs in it that can change its expected behavior. There have been a lot of efforts to automate the process of bug detection but most of the techniques proposed have a high rate of false alarms. Some of these techniques leverage the information available in software code to extract programming patterns that can be used to find potential bugs. Although such an approach has proved to be fruitful for finding bugs but large number of false alarms makes it almost useless in software development. The elements present in a software code have relationships among them formally known as dependencies and the process of finding them is known as dependency analysis. There is a technique known as market basket analysis used by large retailers to find association between items. It works by looking for combinations of items that occur together frequently in transactions. Similarly, in a software code combinations of elements that occur together, can be used to find association between them. This technique is formally known as frequent itemset mining in the data mining domain. This work proposes an approach, named Strip- Miner, that combines dependency analysis with frequent itemset mining to reduce the rate of false alarms. We adopt a two phase approach 1)finding the potential bugs in code and 2)filtering the false alarms. In the first phase we extract code elements and dependencies among them and use frequent itemset mining to find programming patterns where a deviation from these patterns is considered as a potential bug. In the second phase, we use the extracted dependencies to build dependency chains between program elements present in a programming pattern and lack of such a chain is an indication of false alarm. Our evaluation on a set of 7 benchmarks consisting of large software code including version control systems, database management systems, software security libraries and utility software like media players shows that combining simple dependency analysis with frequent itemset mining can significantly decrease the rate of false alarms. Using our approach we are able to reduce the number of generated bugs by up to 99.9% with a false alarms rate of 65.19% and real bugs rate of 34.18% on average as compared to an earlier frequent itemset mining based approach "PR-Miner".

Program testing is an important aspect of software development. Symbolic execution can be used as a tool to automatically verify the correctness of programs for all feasible paths of execution. Moreover, for embedded systems symbolic execution can be used to generate test cases to estimate run times to help determine the worst-case execution time (WCET) and schedulability of systems. This thesis explores an architecture for symbolic execution for use in embedded Rust. Accompanied with the architecture are implementation details of a prototype Symex that can handle small programs. Symex evaluates all feasible paths of execution looking for errors and assertions, and reports which concrete inputs lead to errors. Included with the prototype is a command-line tool to automatically build and analyze Rust projects. The tool allows for easy analysis of projects, and an included library provides functions to manipulate symbolic variables to aid the analysis. The method of evaluating all feasible paths work well with the purpose of evaluating embedded systems, where the aim is typically to keep the code complexity low. The low code complexity lends the software to be resilient towards path explosion. For the cases where this cannot be helped the functions to manipulate the symbolic variables in the analysis can be used to further constrain the variables and lower the number of feasible paths. The evaluation shows the architecture is feasible for the intended use case in embedded systems. Furthermore, evaluation of the prototype shows how the system can be used to show the absence of errors, verify functions, and check for functional equivalence. Inherent to the symbolic execution approach the system cannot handle programs with a large branching factor.

La vérification de programmes avec des calculs sur les nombres à virgule flottante est une étape très importante dans le développement de logiciels critiques. Les calculs sur les nombres flottants sont généralement imprécis, et peuvent dans certains cas diverger par rapport au résultat attendu sur les nombres réels. L’objectif de cette thèse est de concevoir un solveur de contraintes sur les nombres à virgule flottante dédié à la vérification de programmes. Nous présentons dans ce manuscrit une nouvelle méthode de résolution de contraintes sur les flottants. Cette méthode se base principalement sur la sur-approximation des contraintes sur les flottants par des contraintes sur les réels. Cette sur-approximation doit être conservative des solutions sur les flottants. Les contraintes obtenues sont ensuite résolues par un solveur de contraintes sur les réels. Nous avons proposé un algorithme de filtrage des domaines sur les flottants basé sur le concept de la sur-approximation qui utilise des techniques de programmation linéaire. Nous avons aussi proposé une méthode de recherche de solutions basée sur des heuristiques. Cette méthode offre aussi la possibilité de comparer le comportement des programmes par rapport à une spécification sur les réels. Ces méthodes ont été implémentées et expérimentées sur un ensemble de programmes avec du calcul sur les nombres flottants. / The verification of programs with floating-point numbers computation is an important issue in the development of critical software systems. Computations over floating-point numbers are not accurate, and the results may be very different from the expected results over real numbers. The aim of this thesis is to design a constraint solver over floating-point numbers for program verification purposes. We introduce a new method for solving constraints over floating-point numbers. This method is based on an over-approximation of floating-point constraints using constraints over real numbers. This overapproximation is safe, that’s to say it doesn’t loose any solution over the floats. The generated constraints are then solved with a constraint solver over real numbers. We propose a new filtering algorithm using linear programming techniques, which takes advantage of these over-approximations of floating-point constraints. We introduce also new search methods and heuristics to find floating-point solutions of these constraints. Using our implementation, we show on a set of counter-examples the difference of the execution of programs over the floats with the specification over real numbers.

Teaching formal methods is notoriously difficult and is linked to motivation problems among the students; we think that formal methods need to be supported by adequate tools to get better acceptance from the students. One of the goals of the thesis is to build a practical tool to help students to deeply understand the classical programming methodology based on specifications, loop invariants, and decomposition into subproblems advocated by Dijkstra, Gries, and Hoare to name only a few famous computer scientists. Our motivation to build this tool is twofold. On the one hand, we demonstrate that existing verification tools (e.g., ESC/Java, Spark, SMV) are too complex to be used in a pedagogical context; moreover they often lack completeness, (and sometimes, even soundness). On the other hand teaching formal (i.e., rigorous) program construction with pen and paper does not motivate students at all. Thus, since students love to use tools, providing them with a tool that checks not only their programs but also their specifications and the structure of their reasoning seemed appealing to us. Obviously, building such a system is far from an easy task. It may even be thought completely unfeasible to experts in the field. Our approach is to restrict our ambition to a very simple programming language with simple types (limited to finite domains) and arrays. In this context, it is possible to specify problems and subproblems, both clearly and formally, using a specific assertion language based on mathematical logic. It appears that constraint programming over finite domains is especially convenient to check the kind of verification conditions that are needed to express the correctness of imperative programs. However, to conveniently generate the constraint problems equivalent to a given verification condition, we wish to have at hand a powerful language that allows us to interleave constraints generation, constraints solving, and to specify a distribution strategy to overcome the incompleteness of the usual consistency techniques used by finite domain constraint programming. We show in this thesis that the Oz language includes all programming mechanisms needed to reach our goals. Such a tool has been fully implemented and is intended to provide interesting feedback to students learning the programming method: it detects programming and/or reasoning errors and it provides typical counter-examples. We argue that our system is adapted to our pedagogical context and we report on experiments of using the tool with students in a third year programming course.

Thesis (M.S.)--West Virginia University, 1995.

Both J2BP and PANDA tools verify compiled Java programs. By now, these tools are not able to process some programs with specific JVM bytecode instruction sequences in the correct way. We described these instruction sequences and proposed their transformations. We developed the new application, called BytecodeTransformer, based on these propositions. This application transforms compiled Java programs and replaces the problematic instruction sequences with some others. Usage of BytecodeTransformer enlarges the set of programs that can be verified by both J2BP and PANDA. We also evaluated BytecodeTransformer on several Java programs, including own tests and well-known open-source programs. These tests demonstrated the correct functionality of BytecodeTransformer. Powered by TCPDF (www.tcpdf.org)

京都大学 / 0048 / 新制・課程博士 / 博士(情報学) / 甲第22675号 / 情博第728号 / 新制||情||125(附属図書館) / 京都大学大学院情報学研究科通信情報システム専攻 / (主査)教授 五十嵐 淳, 教授 山本 章博, 教授 湊 真一 / 学位規則第4条第1項該当 / Doctor of Informatics / Kyoto University / DFAM