We propose PRECIS, a methodology for automatically generating invariants at function and loop boundaries through program path guided clustering. We instrument function inputs and outputs together with predicates for branch conditions and record their values during each execution. Program runs that share the same path are grouped together based on predicate words. For each group with sufficient data we use linear regression to express the output as a function of the inputs. Groups with insufficient data are examined as candidates for clustering with neighboring groups. Candidates that share the same output function are merged into a cluster. For each cluster, we write an invariant that summarizes the behavior of the corresponding set of paths. We evaluate our technique using Siemens benchmarks. When compared to Daikon, we find that our method has significant advantages.

Embedded control systems consist of multiple components with different criticality levels interacting with each other. For example, in a passenger jet, the navigation system interacts with the passenger entertainment system in providing passengers the distance-to-destination information. It is imperative that failures in the non-critical subsystem should not compromise critical functionality. This architectural principle for robustness can, however, be easily compromised by implementation-level errors. We describe Safe- Flow, which statically analyzes core components in the system to ensure that they use non-core values communicated through shared memory only if they are run-time monitored for safety or recoverability. Using simple, local annotations and semantic restrictions on shared memory usage in the core component, SafeFlow precisely identifies accesses to unmonitored non-core values. With a few false positives, it identifies erroneous dependencies of critical data on noncore values that can arise due to programming errors, inadvertent accesses, or wrong assumptions regarding the absence of difficult-to-detect implementation errors such as data races and synchronization. We demonstrate the utility of SafeFlow by applying it to discover critical value flow dependencies in three prototype systems.

Static analysis of programs in weakly typed languages such as C and C++ is generally not sound because of possible memory errors due to dangling pointer references, uninitialized pointers, and array bounds overflow. We describe a compilation strategy for standard C programs that guarantees that aggressive interprocedural pointer analysis (or less precise ones), a call graph, and type information for a subset of memory, are never invalidated by any possible memory errors. We formalize our approach as a new type system with the necessary run-time checks in operational semantics and prove the correctness of our approach for a subset of C. Our semantics provide the foundation for other sophisticated static analyses to be applied to C programs with a guarantee of soundness. Our work builds on a previously published transformation called Automatic Pool Allocation to ensure that hard-to-detect memory errors (dangling pointer references and certain array bounds errors) cannot invalidate the call graph, points-to information or type information. The key insight behind our approach is that pool allocation can be used to create a run-time partitioning of memory that matches the compile-time memory partitioning in a points-to graph, and efficient checks can be used to isolate the run-time partitions. Furthermore, we show that the sound analysis information enables static checking techniques that eliminate many run-time checks. Our approach requires no source code changes, allows memory to be managedexplicitly, and does not use meta-data on pointers or individual tag bits for memory. Using several benchmark s and system codes, we show experimentally that the run-time overheads are low (less than 10% in nearly all cases and 30% in the worst case we have seen).We also show the effectiveness of static analyses in eliminating run-time checks.

Traditional control systems consist of sensors, controllers, and actuators operating with tight periodic dependencies, and communicating over dedicated real-time channels such as CAN or FDDI. However, best effort networks such as 802.11 are being increasingly used in such systems. The unpredictable delays and losses in such networks violate the periodicity assumptions of digital control design, and the consequent fail-safe actions incur significant performance penalties. In this paper, we propose a co-design based approach to address the periodicity requirements of digital control design, and improve robustness by extending deadlines through graceful degradation to the fail-safe action. In particular, we analytically demonstrate significant deadline extensions in the control loop of a traffic control testbed based on our approach. Such deadline extensions also facilitate fault tolerance techniques such as component restarts, and system management mechanisms such as online component upgrades. We validate the results by experiments in the testbed.

Traditional approaches to enforcing memory safety of programs rely heavily on run-time checks of memory accesses and on garbage collection, both of which are unattractive for embedded applications. The goal of our work is to develop advanced compiler techniques for enforcing memory safety with minimal run-time overheads. In this paper, we describe a set of compiler techniques that, together with minor semantic restrictions on C programs and no new syntax, ensure memory safety and provide most of the error-detection capabilities of type-safe languages, without using garbage collection, and with no run-time software checks, (on systems with standard hardware support for memory management). The language permits arbitrary pointer-based data structures, explicit deallocation of dynamically allocated memory, and restricted array operations. One of the key results of this paper is a compiler technique that ensures that dereferencing dangling pointers to freed memory does not violate memory safety, without annotations, run-time checks, or garbage collection , and works for arbitrary type-safe C programs. Furthermore, we present a new interprocedural analysis for static array bounds checking under certain assumptions. For a diverse set of embedded C programs, we show that we are able to ensure memory safety of pointer and dynamic memory usage in all these programs with no run-time software checks (on systems with standard hardware memory protection), requiring only minor restructuring to conform to simple type restrictions. Static array bounds checking fails for roughly half the programs we study due to complex array references, and these are the only cases where explicit run-time software checks would be needed under our language and system assumptions.

Traditional approaches to enforcing memory safety of programs rely heavily on runtime checks of memory accesses and on garbage collection, both of which are unattractive for embedded applications. The long-term goal of our work is to enable 100% static enforcement of memory safety for embedded programs through advanced compiler techniques and minimal semantic restrictions on programs. The key result of this paper is a compiler technique that ensures memory safety of dynamically allocated memory without programmer annotations, runtime checks, or garbage collection, and works for a large subclass of type-safe C programs. The technique is based on a fully automatic pool allocation (i.e., region-inference) algorithm for C programs we developed previously, and it ensures safety of dynamically allocated memory while retaining explicit deallocation of individual objects within regions (to avoid garbage collection). For a diverse set of embedded C programs (and using a previous technique to avoid null pointer checks), we show that we are able to statically ensure the safety of pointer and dynamic memory usage in all these programs. We also describe some improvements over our previous work in static checking of array accesses. Overall, we achieve 100% static enforcement of memory safety without new language syntax for a significant subclass of embedded C programs, and the subclass is much broader if array bounds checks are ignored. Overall, these techniques greatly expand the class of embedded programs for which 100% static enforcement of memory safety is possible, and furthermore can be achieved without new language support.

This paper considers the problem of providing safe programming support and enabling secure online software upgrades for control software in real-time control systems. In such systems, offline techniques for ensuring code safety are greatly preferable to online techniques. We propose a language called Control-C that is essentially a subset of C, but with key restrictions designed to ensure that memory safety of code can be verified entirely by static checking, under certain system assumptions. The language permits pointer-based data structures, restricted dynamic memory allocation, and restricted array operations, without requiring any runtime checks on memory operations and without garbage collection. The language restrictions have been chosen based on an understanding of both compiler technology and the needs of real-time control systems. The paper describes the language design and a compiler implementation for Control-C. We use control codes from three different experimental control systems to evaluate the suitability of the language for these codes, the effort required to port them to Control-C, and the effectiveness of the compiler in detecting a wide range of potential security violations for one of the systems.