More Like this

1. Relational Symbolic Execution

   https://doi.org/10.1145/3354166.3354175  

   Farina, Gian Pietro; Chong, Stephen; Gaboardi, Marco (October 2019, Proceedings of the 21st International Symposium on Principles and Practice of Programming Languages, PPDP 2019)
2. Symbolic router execution

   https://doi.org/10.1145/3544216.3544264  

   Zhang, Peng; Wang, Dan; Gember-Jacobson, Aaron (August 2022, Proceedings of the ACM SIGCOMM 2022 Conference)

   Network verification often requires analyzing properties across different spaces (header space, failure space, or their product) under different failure models (deterministic and/or probabilistic). Existing verifiers efficiently cover the header or failure space, but not both, and efficiently reason about deterministic or probabilistic failures, but not both. Consequently, no single verifier can support all analyses that require different space coverage and failure models. This paper introduces Symbolic Router Execution (SRE), a general and scalable verification engine that supports various analyses. SRE symbolically executes the network model to discover what we call packet failure equivalence classes (PFECs), each of which characterises a unique forwarding behavior across the product space of headers and failures. SRE enables various optimizations during the symbolic execution, while remaining agnostic of the failure model, so it scales to the product space in a general way. By using BDDs to encode symbolic headers and failures, various analyses reduce to graph algorithms (e.g., shortest-path) on the BDDs. Our evaluation using real and synthetic topologies show SRE achieves better or comparable performance when checking reachability, mining specifications, etc. compared to state-of-the-art methods. 

   more » « less
3. Abstracting Faceted Execution

   https://doi.org/10.1109/CSF49147.2020.00021  

   Micinski, Kristopher; Darais, David; Gilray, Thomas (June 2020, Computer Security Foundations Symposium (CSF))

   null (Ed.)

   Faceted execution is a linguistic paradigm for dynamic information-flow control with the distinguishing feature that program values may be faceted. Such values represent multiple versions or facets at once, for different security labels. This enables policy-agnostic programming: a paradigm permitting expressive privacy policies to be declared, independent of program logic. Although faceted execution prevents information leakage at runtime, it does not guarantee the absence of failure due to policy violations. By contrast with static mechanisms (such as security type systems), dynamic information-flow control permits arbitrarily expressive and dynamic privacy policies but imposes significant runtime overhead and delays discovery of any possible violations. In this paper, we present the two different abstract interpretations for faceted execution in the presence of first-class policies. We first present an abstraction which allows one to reason statically about the shape of facets at each program point. This abstraction is useful for statically proving the absence of runtime errors and eliminating runtime checks related to facets. Reasoning statically about the contents of faceted values, however, is complicated by the presence of first-class security labels, especially because abstract labels may conflate more than one runtime label. To address these issues, we also develop a more precise abstraction that relies on an analysis tracking singleton heap abstractions. We present an implementation of our coarse abstraction in Racket and demonstrate its performance on several sample programs. We conclude by showing how our precise domain can be used to verify information-flow properties. 

   more » « less
4. Feedback-Directed Partial Execution

   https://doi.org/10.1145/3650212.3680320  

   Hayet, Ishrak; Scott, Adam; d'Amorim, Marcelo (September 2024, ACM)
5. Derivative-Guided Symbolic Execution

   https://doi.org/10.1145/3704886  

   Yuan, Yongwei; Zhou, Zhe; Belyakova, Julia; Jagannathan, Suresh (January 2025, Proceedings of the ACM on Programming Languages)

   We consider the formulation of a symbolic execution (SE) procedure for functional programs that interact with effectful, opaque libraries. Our procedure allows specifications of libraries and abstract data type (ADT) methods that are expressed inLinear Temporal Logic over Finite Traces(LTL_f), interpreting them assymbolic finite automata(SFAs) to enable intelligent specification-guided path exploration in this setting. We apply our technique to facilitate the falsification of complex data structure safety properties in terms of effectful operations made by ADT methods on underlying opaque representation type(s). Specifications naturally characterize admissible traces of temporally-ordered events that ADT methods (and the library methods they depend upon) are allowed to perform. We show how to use these specifications to construct feasible symbolic input states for the corresponding methods, as well as how to encode safety properties in terms of this formalism. More importantly, we incorporate the notion ofsymbolic derivatives, a mechanism that allows the SE procedure to intelligently underapproximate the set of precondition states it needs to explore, based on the automata structures latent in the provided specifications and the safety property that is to be falsified. Intuitively, derivatives enable symbolic execution to exploit temporal constraints defined by trace-based specifications to quickly prune unproductive paths and discover feasible error states. Experimental results on a wide-range of challenging ADT implementations demonstrate the effectiveness of our approach. 

   more » « less