Finite Transducers (FTs) extend the capabilities of Finite Au- tomata (FAs) by enabling the transformation of input strings into output strings. In many practical applications — includ- ing program analysis, string constraint solving, and analysis of security-critical sanitizers — Symbolic FTs (SFTs) and Sym- bolic FAs (SFAs) are used instead of the explicitly represented models. To circumvent to the notorious state-space explosion problem caused by an extremely large alphabet size (e.g. Unicode), SFTs and SFAs allow the representation of the alphabet as an effective boolean algebra including finite unions of intervals, as well as SMT-Algebras. The security-critical nature of many of these applications demands trustworthy implementations of such systems. To this end, we present the first formalization of SFTs and their most important algorithms in Isabelle/HOL. To evaluate the effectiveness of our formalization, we apply the formalized SFTs to two applications: (1) sanitizers for web applications used for preventing XSS attacks, and (2) string solving, which increasingly employs intricate string replacement operations. Our experimental results demonstrate that our methods are competitive with the existing unverified implementations.

To formally verify large-scale systems, development and verification needs to be tightly integrated right from the start but this requires tool support that is currently missing. We present a framework for the Rust programming language that utilizes symbolic program execution to bridge the gap between development and verification. A use case provides first evidence that our tool integrates formal verification into the early development cycle and thus has the potential to scale for the verification of large systems.

Theories over strings are among the most heavily researched logical theories in the SMT community in the past decade, owing to the error-prone nature of string manipulations, which often leads to security vulnerabilities (e.g. cross-site scripting and code injection). The majority of the existing decision procedures and solvers for these theories are themselves intricate; they are complicated algorithmically, and also have to deal with a very rich vocabulary of operations. This has led to a plethora of bugs in implementation, which have for instance been discovered through fuzzing.

Regular expressions are a classical concept in formal language theory. Regular expressions in programming languages (RegEx) such as JavaScript, feature non-standard semantics of operators (e.g. greedy/lazy Kleene star), as well as additional features such as capturing groups and references. While symbolic execution of programs containing RegExes appeals to string solvers natively supporting important features of RegEx, such a string solver is hitherto missing. In this paper, we propose the first string theory and string solver that natively provides such support. The key idea of our string solver is to introduce a new automata model, called prioritized streaming string transducers (PSST), to formalize the semantics of RegEx-dependent string functions. PSSTs combine priorities, which have previously been introduced in prioritized finite-state automata to capture greedy/lazy semantics, with string variables as in streaming string transducers to model capturing groups. We validate the consistency of the formal semantics with the actual JavaScript semantics by extensive experiments. Furthermore, to solve the string constraints, we show that PSSTs enjoy nice closure and algorithmic properties, in particular, the regularity-preserving property (i.e., pre-images of regular constraints under PSSTs are regular), and introduce a sound sequent calculus that exploits these properties and performs propagation of regular constraints by means of taking post-images or pre-images. Although the satisfiability of the string constraint language is generally undecidable, we show that our approach is complete for the so-called straight-line fragment. We evaluate the performance of our string solver on over 195000 string constraints generated from an open-source RegEx library. The experimental results show the efficacy of our approach, drastically improving the existing methods (via symbolic execution) in both precision and efficiency.

Abstract The unsafe features of C make it a big challenge to ensure memory safety of C programs, and often lead to memory errors that can result in vulnerabilities. Various formal verification techniques for ensuring memory safety of C have been proposed. However, most of them either have a high overhead, such as state explosion problem in model checking, or have false positives, such as abstract interpretation. In this article, by innovatively borrowing ownership system from Rust, we propose a novel and sound static memory safety analysis approach, named SafeOSL. Its basic idea is an ownership‐based intermediate language, called ownership system language (OSL), which captures the features of the ownership system in Rust. Ownership system specifies the relations among variables and memory locations, and maintains invariants that can ensure memory safety. The semantics of OSL is formalized in K‐framework, which is a rewriting‐logic based tool. C programs to be checked are first transformed into OSL programs and then detected by OSL semantics. Experimental results have demonstrated that SafeOSL is effective in detecting memory errors of C. Moreover, the translations and experiments indicate that the intermediate language OSL could be reused by other programming languages to detect memory errors.

Bitcoin has been a popular research topic recently. Ethereum (ETH), a second generation of cryptocurrency, extends Bitcoin's design by offering a Turing-complete programming language called Solidity to develop smart contracts. Smart contracts allow creditable execution of contracts on EVM (Ethereum Virtual Machine) without third parties. Developing correct and secure smart contracts is challenging due to the decentralized computation nature of the blockchain. Buggy smart contracts may lead to huge financial loss. Furthermore, smart contracts are very hard, if not impossible, to patch once they are deployed. Thus, there is a recent surge of interest in analyzing and verifying smart contracts. While most of the existing works either focus on EVM bytecode or translate Solidity smart contracts into programs in intermediate languages, we argue that it is important and necessary to understand and formally define the semantics of Solidity since programmers write and reason about smart contracts at the level of source code. In this work, we develop a formal semantics for Solidity which provides a formal specification of smart contracts to define semantic-level security properties for the high-level verification. Furthermore, the proposed semantics defines correct and secure high-level execution behaviours of smart contracts to reason about compiler bugs and assist developers in writing secure smart contracts.

Buddy memory allocation algorithms are widely adopted by various memory management systems for managing memory layouts. Rigorous mathematical proofs provide strong assurance to improve the confidence on the reliability of a memory management system. In this paper, we model and formally verify, in the interactive theorem prover Isabelle/HOL, a buddy memory allocation model, which preserves functional correctness and security properties. Firstly, we construct a specification consisting of operations to allocate and dispose memory blocks according to a buddy memory allocation algorithm. Then we verify that the specification preserves key invariants over the memory to guarantee functional correctness of the algorithm. Finally, we verify that the specification also preserves the integrity of the memory. Therefore, they do not affect other memory blocks previously allocated.

The unsafe language features of C, such as low-level control of memory, often lead to memory errors, which can result in silent data corruption, security vulnerabilities, and program crashes. Dynamic analysis tools, which have been widely used for detecting memory errors at runtime, usually perform instrumentation at the IR-level or binary-level. However, their underlying non-source-level instrumentation techniques have three inherent limitations: optimization sensitivity, platform dependence and DO-178C non-compliance. Due to optimization sensitivity, these tools are used to trade either performance for effectiveness by compiling the program at -O0 or effectiveness for performance by compiling the program at a higher optimization level, say, -O3.

State/event linear temporal logic (SE-LTL) provides a concise and intuitive way to express properties incorporating both states and events. Automata-theoretic LTL model checking can be applied to verify SE-LTL properties. However, as SE-LTL is not preserved under classical stutter-equivalence, conventional partial order reduction (POR) cannot be directly used to check them. In this paper, we propose a novel approach to exploit POR for reducing the state space with respect to SE-LTL formulas. This approach detects a ‘state part’ of a Büchi automaton (BA) translated from an SE-LTL formula. Based on ‘state part’, we introduce a definition of SPs of BAs and labeled Kripke structures (LKS) with the integration of POR for reducing the state spaces of the products. The integrated POR modifies conventional POR by introducing an identification of visible actions with respect to events. Moreover, in order to apply POR to the full class of SE-LTL, we provide techniques to exploit POR for checking SE-LTL with the nexttime operator. We have implemented our techniques in SPIN model checker. The experimental results illustrate the potential of the techniques for reduction compared with pure state-based model checking and SE-LTL model checking without POR.

Summary With rapid development in software technology, more and more safety‐critical systems are software intensive. Safety issues become important when software is used to control such systems. However, there are 2 important problems in software safety analysis: (1) there is often a significant traceability gap between safety requirements and software design, resulting in safety analysis and software design are often conducted separately; and (2) the growing complexity of safety‐critical software makes it difficult to determine whether software design fulfills safety requirements. In this paper, we propose a technique to address the above 2 important problems on the model level. The technique is based on statecharts, which are used to model the behavior of software, and fault tree safety analysis. This technique contains the following 2 parts, which are corresponding to the 2 problems, respectively. The first part is to build a metamodel of traceability between fault trees and statecharts, which is to bridge their traceability gap. A collection of rules for the creation and maintenance of traceability links is provided. The second part is a model slicing technique to reduce the complexity of statecharts with respect to the traceability information. The slicing technique can deal with the characteristics of hierarchy, concurrency, and synchronization of statecharts. The reduced statecharts are much smaller than their original statecharts, which are helpful to successive safety analysis. Finally, we illustrate the effectiveness and the importance of the method by a case study of slats and flaps control units in flight control systems.

In this paper, we are concerned by the elaboration of generic development steps for the code generation for synchronous languages. Our aim is to provide a correct by construction solution. For that purpose, we adopt a refinement-based approach where proof obligations for each step guarantee properties preservation. We use the Event-B formal method. We start with a big step semantics specified by an Event-B machine. Through a sequence of refinements, expressed as Event-B refinement machines, we end up with a code generation step which implements a small step semantics preserving the properties of the big step semantics.

Ensuring safety-critical software safety requires strict verification of the conformance between safety requirements and programs. Formal verification techniques, such as model checking and theorem proving, can be used to partially realize this objective. DO-178C, a standard for airborne systems, allows formal verification techniques to replace certain forms of testing. My research is concerned with applying model checking to verify the conformance between safety requirements and programs. First, a formal language for specifying software safety requirements which are relevant to event sequences is introduced. Second, the traceability information models between formalized safety requirements and programs are built. Third, the checking of a program against a safety requirement is decomposed into smaller model checking problems by utilizing traceability information model between them.