José F. Morales

Yuliya Lierler, Jose F. Morales, Carmine Dodaro et al.

ICLP is the premier international event for presenting research in logic programming. Contributions to ICLP 2022 were sought in all areas of logic programming, including but not limited to: Foundations: Semantics, Formalisms, Nonmonotonic reasoning, Knowledge representation. Languages issues: Concurrency, Objects, Coordination, Mobility, Higher order, Types, Modes, Assertions, Modules, Meta-programming, Logic-based domain-specific languages, Programming techniques. Programming support: Program analysis, Transformation, Validation, Verification, Debugging, Profiling, Testing, Execution visualization. Implementation: Compilation, Virtual machines, Memory management, Parallel and Distributed execution, Constraint handling rules, Tabling, Foreign interfaces, User interfaces. Related Paradigms and Synergies: Inductive and coinductive logic programming, Constraint logic programming, Answer set programming, Interaction with SAT, SMT and CSP solvers, Theorem proving, Argumentation, Probabilistic programming, Machine learning. Applications: Databases, Big data, Data integration and federation, Software engineering, Natural language processing, Web and semantic web, Agents, Artificial intelligence, Computational life sciences, Cyber-security, Robotics, Education.

Xaver Fabian, Marco Guarnieri, Boris Köpf et al.

Speculative execution enhances processor performance by predicting intermediate results and executing instructions based on these predictions. However, incorrect predictions can lead to security vulnerabilities, as speculative instructions leave traces in microarchitectural components that attackers can exploit. This is demonstrated by the family of Spectre attacks. Unfortunately, existing countermeasures to these attacks lack a formal security characterization, making it difficult to verify their effectiveness. In this paper, we propose a novel framework for detecting information flows introduced by speculative execution and reasoning about software defenses. The theoretical foundation of our approach is speculative non-interference (SNI), a novel semantic notion of security against speculative execution attacks. SNI relates information leakage observed under a standard non-speculative semantics to leakage arising under semantics that explicitly model speculative execution. To capture their combined effects, we extend our framework with a mechanism to safely compose multiple speculative semantics, each focussing on a single aspect of speculation. This allows us to analyze the complex interactions and resulting leaks that can arise when multiple speculative mechanisms operate together. On the practical side, we develop Spectector, a symbolic analysis tool that uses our compositional framework and leverages SMT solvers to detect vulnerabilities and verify program security with respect to multiple speculation mechanisms. We demonstrate the effectiveness of Spectector through evaluations on standard security benchmarks and new vulnerability scenarios.

Marco Guarnieri, Boris Köpf, José F. Morales et al.

Since the advent of SPECTRE, a number of countermeasures have been proposed and deployed. Rigorously reasoning about their effectiveness, however, requires a well-defined notion of security against speculative execution attacks, which has been missing until now. In this paper (1) we put forward speculative non-interference, the first semantic notion of security against speculative execution attacks, and (2) we develop SPECTECTOR, an algorithm based on symbolic execution to automatically prove speculative non-interference, or to detect violations. We implement SPECTECTOR in a tool, which we use to detect subtle leaks and optimizations opportunities in the way major compilers place SPECTRE countermeasures. A scalability analysis indicates that checking speculative non-interference does not exhibit fundamental bottlenecks beyond those inherited by symbolic execution.

Pepe Vila, Boris Köpf, José Francisco Morales

Many micro-architectural attacks rely on the capability of an attacker to efficiently find small eviction sets: groups of virtual addresses that map to the same cache set. This capability has become a decisive primitive for cache side-channel, rowhammer, and speculative execution attacks. Despite their importance, algorithms for finding small eviction sets have not been systematically studied in the literature. In this paper, we perform such a systematic study. We begin by formalizing the problem and analyzing the probability that a set of random virtual addresses is an eviction set. We then present novel algorithms, based on ideas from threshold group testing, that reduce random eviction sets to their minimal core in linear time, improving over the quadratic state-of-the-art. We complement the theoretical analysis of our algorithms with a rigorous empirical evaluation in which we identify and isolate factors that affect their reliability in practice, such as adaptive cache replacement strategies and TLB thrashing. Our results indicate that our algorithms enable finding small eviction sets much faster than before, and under conditions where this was previously deemed impractical.