More Like this

1. Model Checking Race-Freedom When “Sequential Consistency for Data-Race-Free Programs” is Guaranteed

   https://doi.org/10.1007/978-3-031-37703-7_13  

   Wu, Wenhao; Hückelheim, Jan; Hovland, Paul D.; Luo, Ziqing; Siegel, Stephen F. (July 2023, International Conference on Computer Aided Verification)

   Enea, Constantin; Lal, Akash (Ed.)

   Many parallel programming models guarantee that if all sequentially consistent (SC) executions of a program are free of data races, then all executions of the program will appear to be sequentially consistent. This greatly simplifies reasoning about the program, but leaves open the question of how to verify that all SC executions are race-free. In this paper, we show that with a few simple modifications, model checking can be an effective tool for verifying race-freedom. We explore this technique on a suite of C programs parallelized with OpenMP. 

   more » « less
2. Recursive Reinforcement Learning

   Hahn, Ernst Moritz; Perez, Mateo; Schewe, Sven; Somenzi, Fabio; Trivedi, Ashutosh; Wojtczak, Dominik (November 2022, Conference on Neural Information Processing Systems (NeurIPS 2022))

   Koyejo, S; Mohamed, S.; Agarwal, A.; Belgrave, D.; Cho, K.; Oh, A. (Ed.)

   Recursion is the fundamental paradigm to finitely describe potentially infinite objects. As state-of-the-art reinforcement learning (RL) algorithms cannot directly reason about recursion, they must rely on the practitioner's ingenuity in designing a suitable "flat" representation of the environment. The resulting manual feature constructions and approximations are cumbersome and error-prone; their lack of transparency hampers scalability. To overcome these challenges, we develop RL algorithms capable of computing optimal policies in environments described as a collection of Markov decision processes (MDPs) that can recursively invoke one another. Each constituent MDP is characterized by several entry and exit points that correspond to input and output values of these invocations. These recursive MDPs (or RMDPs) are expressively equivalent to probabilistic pushdown systems (with call-stack playing the role of the pushdown stack), and can model probabilistic programs with recursive procedural calls. We introduce Recursive Q-learning---a model-free RL algorithm for RMDPs---and prove that it converges for finite, single-exit and deterministic multi-exit RMDPs under mild assumptions. 

   more » « less
3. Witnessability of Undecidable Problems

   https://doi.org/10.1145/3571227  

   Ding, Shuo; Zhang, Qirun (January 2023, Proceedings of the ACM on Programming Languages)

   Many problems in programming language theory and formal methods are undecidable, so they cannot be solved precisely. Practical techniques for dealing with undecidable problems are often based on decidable approximations. Undecidability implies that those approximations are always imprecise. Typically, practitioners use heuristics andad hocreasoning to identify imprecision issues and improve approximations, but there is a lack of computability-theoretic foundations about whether those efforts can succeed. This paper shows a surprising interplay between undecidability and decidable approximations: there exists a class of undecidable problems, such that it is computable to transform any decidable approximation to a witness input demonstrating its imprecision. We call those undecidable problemswitnessable problems. For example, if a program propertyPis witnessable, then there exists a computable functionf_P, such thatf_Ptakes as input the code of any program analyzer targetingPand produces an input programwon which the program analyzer is imprecise. An even more surprising fact is that the class of witnessable problems includes almost all undecidable problems in programming language theory and formal methods. Specifically, we prove the diagonal halting problemKis witnessable, and the class of witnessable problems is closed under complements and many-one reductions. In particular, all “non-trivial semantic properties of programs” mentioned in Rice’s theorem are witnessable. We also explicitly construct a problem in the non-witnessable (and undecidable) class and show that both classes have cardinality 2^ℵ₀. Our results offer a new perspective on the understanding of undecidability: for witnessable problems, although it is impossible to solve them precisely, it is always possible to improve any decidable approximation to make it closer to the precise solution. This fact formally demonstrates that research efforts on such approximations are promising and shows there exist universal ways to identify precision issues of program analyzers, program verifiers, SMT solvers, etc., because their essences are decidable approximations of witnessable problems. 

   more » « less
4. Deciding Branching Hyperproperties for Real Time Systems

   https://doi.org/10.1109/CSF61375.2024.00032  

   Deka, Nabarun; Zhang, Minjian; Chadha, Rohit; Viswanathan, Mahesh (July 2024, IEEE 37th Computer Security Foundations Symposium (CSF))

   Security properties of real-time systems often involve reasoning about hyper-properties, as opposed to properties of single executions or trees of executions. These hyper-properties need to additionally be expressive enough to reason about real-time constraints. Examples of such properties include information flow, side channel attacks and service-level agreements. In this paper we study computational problems related to a branching-time, hyper-property extension of metric temporal logic (MTL) that we call HCMTL*. We consider both the interval-based and point-based semantics of this logic. The verification problem that we consider is to determine if a given HCMTL* formula ℑ is true in a system represented by a timed automaton. We show that this problem is undecidable. We then show that the verification problem is decidable if we consider executions upto a fixed time horizon T. Our decidability result relies on reducing the verification problem to the truth of an MSO formula over reals with a bounded time interval. 

   more » « less
5. Iodine: Fast Dynamic Taint Tracking Using Rollback-free Optimistic Hybrid Analysis

   https://doi.org/10.1109/SP.2019.00043  

   Banerjee, Subarno; Devecsery, David; Chen, Peter M.; Narayanasamy, Satish (May 2019, IEEE Symposium on Security and Privacy)

   Dynamic information-flow tracking (DIFT) is useful for enforcing security policies, but rarely used in practice, as it can slow down a program by an order of magnitude. Static program analyses can be used to prove safe execution states and elide unnecessary DIFT monitors, but the performance improvement from these analyses is limited by their need to maintain soundness. In this paper, we present a novel optimistic hybrid analysis (OHA) to significantly reduce DIFT overhead while still guaranteeing sound results. It consists of a predicated whole-program static taint analysis, which assumes likely invariants gathered from profiles to dramatically improve precision. The optimized DIFT is sound for executions in which those invariants hold true, and recovers to a conservative DIFT for executions in which those invariants are false. We show how to overcome the main problem with using OHA to optimize live executions, which is the possibility of unbounded rollbacks. We eliminate the need for any rollback during recovery by tailoring our predicated static analysis to eliminate only safe elisions of noop monitors. Our tool, Iodine, reduces the overhead of DIFT for enforcing security policies to 9%, which is 4.4x lower than that with traditional hybrid analysis, while still being able to be run on live systems. 

   more » « less