More Like this

1. VSTlib: Library Components for Verified C Programs

   Appel, Andrew W (August 2024, Coq Workshop)

   Bertot, Yves; Enrico, Tassi (Ed.)

   C program components verified for functional correctness in Coq using VST (Verified Software Toolchain) can now rely on a set of standard library components (math functions, malloc/free, atomic load/store, locks, threads) that have formal specifications. 

   more » « less
2. Connecting Higher-Order Separation Logic to a First-Order Outside World

   https://doi.org/10.1007/978-3-030-44914-8_16  

   William Mansky, Wolf Honoré (April 2020, Programming Languages and Systems. ESOP 2020)

   Separation logic is a useful tool for proving the correctness of programs that manipulate memory, especially when the model of memory includes higher-order state: Step-indexing, predicates in the heap, and higher-order ghost state have been used to reason about function pointers, data structure invariants, and complex concurrency patterns. On the other hand, the behavior of system features (e.g., operating systems) and the external world (e.g., communication between components) is usually specified using first-order formalisms. In principle, the soundness theorem of a separation logic is its interface with first-order theorems, but the soundness theorem may implicitly make assumptions about how other components are specified, limiting its use. In this paper, we show how to extend the higher-order separation logic of the Verified Software Toolchain to interface with a first-order verified operating system, in this case CertiKOS, that mediates its interaction with the outside world. The resulting system allows us to prove the correctness of C programs in separation logic based on the semantics of system calls implemented in CertiKOS. It also demonstrates that the combination of interaction trees + CompCert memories serves well as a lingua franca to interface and compose two quite different styles of program verification. 

   more » « less
3. Virtual timeline: a formal abstraction for verifying preemptive schedulers with temporal isolation

   https://doi.org/10.1145/3371088  

   Liu, Mengqi; Rieg, Lionel; Shao, Zhong; Gu, Ronghui; Costanzo, David; Kim, Jung-Eun; Yoon, Man-Ki (December 2019, Proceedings of the ACM on Programming Languages)

   The reliability and security of safety-critical real-time systems are of utmost importance because the failure of these systems could incur severe consequences (e.g., loss of lives or failure of a mission). Such properties require strong isolation between components and they rely on enforcement mechanisms provided by the underlying operating system (OS) kernel. In addition to spatial isolation which is commonly provided by OS kernels to various extents, it also requires temporal isolation, that is, properties on the schedule of one component (e.g., schedulability) are independent of behaviors of other components. The strict isolation between components relies critically on algorithmic properties of theconcrete implementationof the scheduler, such as timely provision of time slots, obliviousness to preemption, etc. However, existing work either only reasons about an abstract model of the scheduler, or proves properties of the scheduler implementation that are not rich enough to establish the isolation between different components. In this paper, we present a novel compositional framework for reasoning about algorithmic properties of the concrete implementation of preemptive schedulers. In particular, we usevirtual timeline, a variant of the supply bound function used in real-time scheduling analysis, to specify and reason about the scheduling of each component in isolation. We show that the properties proved on this abstraction carry down to the generated assembly code of the OS kernel. Using this framework, we successfully verify a real-time OS kernel, which extends mCertiKOS, a single-processor non-preemptive kernel, with user-level preemption, a verified timer interrupt handler, and a verified real-time scheduler. We prove that in the absence of microarchitectural-level timing channels, this new kernel enjoys temporal and spatial isolation on top of the functional correctness guarantee. All the proofs are implemented in the Coq proof assistant. 

   more » « less
4. CompCertO: Compiling Certified Open C Components

   https://doi.org/10.1145/3453483.3454097  

   Koenig, Jérémie; Shao, Zhong (June 2021, Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI'21))

   Since the introduction of CompCert, researchers have been refining its language semantics and correctness theorem, and used them as components in software verification efforts. Meanwhile, artifacts ranging from CPU designs to network protocols have been successfully verified, and there is interest in making them interoperable to tackle end-to-end verification at an even larger scale. Recent work shows that a synthesis of game semantics, refinement-based methods, and abstraction layers has the potential to serve as a common theory of certified components. Integrating certified compilers to such a theory is a critical goal. However, none of the existing variants of CompCert meets the requirements we have identified for this task. CompCertO extends the correctness theorem of CompCert to characterize compiled program components directly in terms of their interaction with each other. Through a careful and compositional treatment of calling conventions, this is achieved with minimal effort. 

   more » « less
5. Wireless batteryless soft sensors for ambulatory cardiovascular health monitoring

   https://doi.org/10.20517/ss.2023.17  

   Guess, Matthew; Soltis, Ira; Rigo, Bruno; Zavanelli, Nathan; Kapasi, Sara; Kim, Hyeonseok; Yeo, Woon-Hong (January 2023, Soft Science)

   Seismocardiography (SCG) is the measure of local vibrations in the chest due to heartbeats. Typically, SCG signals are measured using rigid integrated circuit (IC) accelerometers and bulky electronics. However, as alternatives, recent studies of emerging flexible sensors show promise. Here, we introduce the development of wireless soft capacitive sensors that require no battery or rigid IC components for measuring SCG signals for cardiovascular health monitoring. Both the capacitive and inductive components of the circuit are patterned with laser micromachining of a polyimide-coated copper and are encapsulated with an elastomer. The wearable soft sensor can detect small strain changes on the skin, which is wirelessly measured by examining the power reflected from the antenna at a stimulating frequency. The performance of the device is verified by comparing the fiducial points to SCG measured by a commercial accelerometer and electromyograms from a commercial electrode. Overall, the human subject study demonstrates that the fiducial points are consistent with data from commercial devices, showing the potential of the ultrathin soft sensors for ambulatory cardiovascular monitoring without bulky electronics and rigid components. 

   more » « less