Aspect-Oriented Programming (AOP) is a programming paradigm that implements crosscutting concerns in a modular way. People have witnessed the prosperity of AOP languages for Java and C++, such as AspectJ and AspectC++, which has propelled AOP to become an important programming paradigm with many interesting application scenarios, e.g., runtime verification. In contrast, the AOP languages for C are still poor and lack compiler support. In this paper, we design a new general-purpose and expressive aspect-oriented C programming language, namely Aclang, and implement a compiler for it, which brings fully-fledged AOP support into the C domain. We have evaluated the effectiveness and performance of our compiler against two state-of-the-art tools, ACC and AspectC++. In terms of effectiveness, Aclang outperforms ACC and AspectC++. In terms of performance, Aclang outperforms ACC in execution time and outperforms AspectC++ in both execution time and memory consumption.

C is a dominant programming language for implementing system and low-level embedded software. Unfortunately, the unsafe nature of its low-level control of memory often leads to memory errors. Dynamic analysis has been widely used to detect memory errors at runtime. However, existing monitoring algorithms for dynamic analysis are not yet satisfactory, as they cannot deterministically and completely detect some types of errors, such as segment confusion errors, sub-object overflows, use-after-frees and memory leaks. We propose a new monitoring algorithm, namely Smatus , short for smart status , that improves memory safety by performing comprehensive dynamic analysis. The key innovation is to maintain at runtime a small status node for each memory object. A status node records the status value and reference count of an object, where the status value denotes the liveness and segment type of this object, and the reference count tracks the number of pointer variables pointing to this object. Smatus maintains at runtime a pointer metadata for each pointer variable, to record not only the base and bound of a pointer’s referent but also the address of the referent’s status node. All the pointers pointing to the same referent share the same status node in their pointer metadata. A status node is smart in the sense that it is automatically deleted when it becomes useless (indicated by its reference count reaching zero). To the best of our knowledge, Smatus represents the most comprehensive approach of its kind. We have evaluated Smatus by using a large set of programs including the NIST Software Assurance Reference Dataset, MSBench, MiBench, SPEC and stress testing benchmarks. In terms of effectiveness (detecting different types of memory errors), Smatus outperforms state-of-the-art tools, Google’s AddressSanitizer, SoftBoundCETS and Valgrind, as it is capable of detecting more errors. In terms of performance (the time and memory overheads), Smatus outperforms SoftBoundCETS and Valgrind in terms of both lower time and memory overheads incurred, and is on par with AddressSanitizer in terms of the time and memory overhead tradeoff made (with much lower memory overheads incurred).

Memory safety issues are the intrinsic diseases of C/C++ programs. Dynamic memory safety enforcement as the dominant approach has an advantage in high effectiveness, yet suffers from prohibitively high runtime overhead. Existing attempts to reduce the overhead are either labor-intensive, tightly dependent on specific hardware/compiler support, or poorly effective.

Low-level control makes C unsafe, resulting in memory errors that can lead to data corruption, security vulnerabilities or program crashes. Dynamic analysis tools, which have been widely used for detecting memory errors at runtime, usually perform instrumentation at the IR or binary level. However, these non-source-level instrumentation frameworks and tools suffer from two inherent drawbacks: optimization sensitivity and platform dependence. Due to optimization sensitivity, the user of these tools must trade either performance for effectiveness by compiling the program at-O0or effectiveness for performance by compiling the program at a higher optimization level, say,-O3. In this paper, we propose a new source-level instrumentation framework to overcome these two drawbacks, and implement it in a new dynamic analysis tool, calledMovec, that adopts a pointer-based monitoring algorithm. We have evaluatedMoveccomprehensively by using the NIST's SARD benchmark suite (1152 programs), a set of 126 microbenchmarks (with ground truth), a set of 20 MiBench benchmarks and 5 pure-C SPEC CPU 2017 benchmarks. In terms of effectiveness,Movecoutperforms three state-of-the-art dynamic analysis tools, AddressSanitizer, SoftBoundCETS and Valgrind, for all the standard optimization levels (from-O0to-O3). In terms of performance,Movecoutperforms SoftBoundCETS and Valgrind, and is slower than AddressSanitizer but consumes less memory.

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.

C is a dominant language for implementing system software. Unfortunately, its support for low-level control of memory often leads to memory errors. Dynamic analysis tools, which have been widely used for detecting memory errors at runtime, are not yet satisfactory as they cannot deterministically and completely detect some types of memory errors, e.g., segment confusion errors, sub-object overflows, use-after-frees, and memory leaks.

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.

In fault injection, we can use a logical constraint as an interface description and negate the constraint to derive logically unreasonable faulty data in order to test the dependability of a system. However, the existing constraint-based approaches only use constraint solving to generate brand new data for testing. Because the given constraints are often incomplete, such brand new data may not satisfy all the hidden constraints and hence can be nonrealistic. Besides, there can be many different strategies to negate a constraint in order to derive constraint-unsatisfied faulty data. Which negation strategy is the best choice for high coverage fault injection is still unclear. To these ends, this paper presents a new constraint-based fault injection technique which relaxes the constraint variables instead of solving brand new data for fault injection. With such an approach, the generated data can be more close to the original non-faulty data and hence are likely to be more realistic. We also investigated the effectiveness of different negation strategies on a constraint formula for fault injection. The experimental results indicate that our constraint relaxing approach does produce faulty data closer to the original ones. The results also provide insights for the application of constraint negation strategies in fault injection.

Many runtime verification tools are built based on Aspect-Oriented Programming (AOP) tools, most often AspectJ, a mature implementation of AOP for Java. Although already popular in the Java domain, there is few work on runtime verification of C programs via AOP, due to the lack of a solid language and tool support. In this paper, we propose a new general purpose and expressive language for defining monitors as an extension to the C language, and present our tool implementation of the weaver, the Movec compiler, which brings fully-fledged parametric runtime verification support into the C domain. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Runtime monitoring can be used to verify, enforce and control the dynamic execution of a target program at runtime to detect property violations, enforce desired properties and actively correct the execution, respectively. However, the state-of-the-art study lacks an appropriate formal program semantics of runtime monitoring. In this paper, we propose a theory of runtime control at an appropriate level of formalization to provide a formal program semantics of instrumented target programs under the control of controlling programs. Our theory provides a complete formal semantics for real implementations of runtime monitoring and control, but still retains a good balance between implementation and generality. Indeed, the theory encompasses the formalization of key implementation techniques, such as program instrumentation, synchronization on passively monitored actions, and synthesis of controlling programs from specifications. On the other hand, the theory is so generic and expressive that many existing formalisms about runtime monitoring can be considered as special cases of our theory.

This work is primarily inspired by the observation that supervisory control and regulated rewriting have the same nature. Indeed, both of them model a system using some formalism and use a certain formalized control structure to restrict the behavior of the system via some designated control mechanisms. In this paper, we propose the theory of Control Systems (C Systems), which provides a more generic framework to integrate the automaton and grammar representations of control in supervisory control and regulated rewriting. The C system contains two components: the controlled component and the controlling component. The two components are expressed using the same formalism, e.g. automata or grammars. More specifically, we define three types of control systems based on the automaton or grammar representation, namely Automaton Control Systems (AC Systems), Grammar Control Systems (GC Systems) and Leftmost-derivation-based Grammar Control Systems (LGC Systems). We formally study their key theoretical characterizations, such as generative power, equivalence and translation techniques, as well as their connections with supervisory control and regulated rewriting, including the relationships between AC systems and supervisory control, and between GC/LGC systems and regulated rewriting. We also discuss some applications of C systems and finally propose some open questions.

Summary This paper documents an application of model checking to formally verify an interrupt‐driven Slats and Flaps Control Unit software programmed in C, one component of a certain type of Chinese aircraft. Our objective was to identify errors rather than to prove correctness. We focused on the correctness of the algorithms used in the buffer operations, which are very common and important in aircraft software. In the verification, a total of four flawed code fragments was identified, including a minor efficiency issue. According to the programming team, this is regarded as a very successful result, and this project is the first successful attempt to apply model checking to the practice of verifying onboard aircraft software in China. Thanks to its completeness and reality, this case study can also serve as a complete and valuable real‐world example for teaching and learning model checking. Copyright © 2013 John Wiley & Sons, Ltd.

Vehicular Ad hoc Networks (VANETs) are a killer application of Mobile Ad hoc Networks (MANETs), which exchange data among vehicles and vehicles to roadside infrastructures by routing. To save energy, various routing protocols for VANETs have been proposed in recent years. However, VANETs impose challenging issues to routing. These issues consist of dynamical road topology, various road obstacles, high vehicle movement and the fact that the vehicle movement is constrained on roads and traffic conditions. Moreover, the movement is significantly influenced by driving behaviors and vehicle categories. To this end, we incorporate them into routing and propose energy-efficient routing using movement trends (ERBA) for VANETs—an energy-efficient routing protocol. ERBA classifies vehicles into several categories, and then leverages vehicle movement trends to make routing recommendation. It predicts the movement trends by current directions and next directions after going through the road intersections. With the vehicular category information, the driving behavior patterns, the distance between the current sections and the next intersections, ERBA propagates information among vehicles with less energy consumption. The proposed scheme is validated by real urban scenarios extracted from ShanghaiGrid project. Experimental results show that ERBA outperforms the compared routing protocols with respect to the end-end delay, the packet delivery ratio and the path duration time.

An ω-grammar is a formal grammar used to generate ω-words (i.e. infinite length words), while an ω-automaton is an automaton used to recognize ω-words. This paper gives clean and uniform definitions for ω-grammars and ω-automata, provides a systematic study of the generative power of ω-grammars with respect to ω-automata, and presents a complete set of results for various types of ω-grammars and acceptance modes. We use the tuple (σ, ρ, π) to denote various acceptance modes, where σ denotes that some designated elements should appear at least once or infinitely often, ρ denotes some binary relation between two sets, and π denotes normal or leftmost derivations. Technically, we propose (σ, ρ, π)-accepting ω-grammars, and systematically study their relative generative power with respect to (σ, ρ)-accepting ω-automata. We show how to construct some special forms of ω-grammars, such as ϵ-production-free ω-grammars. We study the equivalence or inclusion relations between ω-grammars and ω-automata by establishing the translation techniques. In particular, we show that, for some acceptance modes, the generative power of ω-CFG is strictly weaker than ω-PDA, and the generative power of ω-CSG is equal to ω-TM (rather than linear-bounded ω-automata-like devices). Furthermore, we raise some remaining open problems for two of the acceptance modes.

The research is motivated by the challenge from the evolution of safety requirements, which leads to revision of system designs at design-time or post-implementation at a high cost. This paper proposes a complementary methodology, namely the model monitoring approach, to better support the evolution throughout the life-cycle at a lower cost.