-
Algorithm-assisted discovery of an intrinsic order among mathematical constants
Authors:
Rotem Elimelech,
Ofir David,
Carlos De la Cruz Mengual,
Rotem Kalisch,
Wolfgang Berndt,
Michael Shalyt,
Mark Silberstein,
Yaron Hadad,
Ido Kaminer
Abstract:
In recent decades, a growing number of discoveries in fields of mathematics have been assisted by computer algorithms, primarily for exploring large parameter spaces that humans would take too long to investigate. As computers and algorithms become more powerful, an intriguing possibility arises - the interplay between human intuition and computer algorithms can lead to discoveries of novel mathem…
▽ More
In recent decades, a growing number of discoveries in fields of mathematics have been assisted by computer algorithms, primarily for exploring large parameter spaces that humans would take too long to investigate. As computers and algorithms become more powerful, an intriguing possibility arises - the interplay between human intuition and computer algorithms can lead to discoveries of novel mathematical concepts that would otherwise remain elusive. To realize this perspective, we have developed a massively parallel computer algorithm that discovers an unprecedented number of continued fraction formulas for fundamental mathematical constants. The sheer number of formulas discovered by the algorithm unveils a novel mathematical structure that we call the conservative matrix field. Such matrix fields (1) unify thousands of existing formulas, (2) generate infinitely many new formulas, and most importantly, (3) lead to unexpected relations between different mathematical constants, including multiple integer values of the Riemann zeta function. Conservative matrix fields also enable new mathematical proofs of irrationality. In particular, we can use them to generalize the celebrated proof by Apéry for the irrationality of $ζ(3)$. Utilizing thousands of personal computers worldwide, our computer-supported research strategy demonstrates the power of experimental mathematics, highlighting the prospects of large-scale computational approaches to tackle longstanding open problems and discover unexpected connections across diverse fields of science.
△ Less
Submitted 16 October, 2023; v1 submitted 22 August, 2023;
originally announced August 2023.
-
Hide and Seek with Spectres: Efficient discovery of speculative information leaks with random testing
Authors:
Oleksii Oleksenko,
Marco Guarnieri,
Boris Köpf,
Mark Silberstein
Abstract:
Attacks like Spectre abuse speculative execution, one of the key performance optimizations of modern CPUs. Recently, several testing tools have emerged to automatically detect speculative leaks in commercial (black-box) CPUs. However, the testing process is still slow, which has hindered in-depth testing campaigns, and so far prevented the discovery of new classes of leakage.
In this paper, we i…
▽ More
Attacks like Spectre abuse speculative execution, one of the key performance optimizations of modern CPUs. Recently, several testing tools have emerged to automatically detect speculative leaks in commercial (black-box) CPUs. However, the testing process is still slow, which has hindered in-depth testing campaigns, and so far prevented the discovery of new classes of leakage.
In this paper, we identify the root causes of the performance limitations in existing approaches, and propose techniques to overcome these limitations. With these techniques, we improve the testing speed over the state-of-the-art by up to two orders of magnitude.
These improvements enable us to run a testing campaign of unprecedented depth on Intel and AMD CPUs. As a highlight, we discover two types of previously unknown speculative leaks (affecting string comparison and division) that have escaped previous manual and automatic analyses.
△ Less
Submitted 18 January, 2023;
originally announced January 2023.
-
Securing Access to Untrusted Services From TEEs with GateKeeper
Authors:
Meni Orenbach,
Bar Raveh,
Alon Berkenstadt,
Yan Michalevsky,
Shachar Itzhaky,
Mark Silberstein
Abstract:
Applications running in Trusted Execution Environments (TEEs) commonly use untrusted external services such as host File System. Adversaries may maliciously alter the normal service behavior to trigger subtle application bugs that would have never occurred under correct service operation, causing data leaks and integrity violations. Unfortunately, existing manual protections are incomplete and ad-…
▽ More
Applications running in Trusted Execution Environments (TEEs) commonly use untrusted external services such as host File System. Adversaries may maliciously alter the normal service behavior to trigger subtle application bugs that would have never occurred under correct service operation, causing data leaks and integrity violations. Unfortunately, existing manual protections are incomplete and ad-hoc, whereas formally-verified ones require special expertise.
We introduce GateKeeper, a framework to develop mitigations and vulnerability checkers for such attacks by leveraging lightweight formal models of untrusted services. With the attack seen as a violation of a services' functional correctness, GateKeeper takes a novel approach to develop a comprehensive model of a service without requiring formal methods expertise. We harness available testing suites routinely used in service development to tighten the model to known correct service implementation. GateKeeper uses the resulting model to automatically generate (1) a correct-by-construction runtime service validator in C that is linked with a trusted application and guards each service invocation to conform to the model; and (2) a targeted model-driven vulnerability checker for analyzing black-box applications.
We evaluate GateKeeper on Intel SGX enclaves. We develop comprehensive models of a POSIX file system and OS synchronization primitives while using thousands of existing test suites to tighten their models to the actual Linux implementations. We generate the validator and integrate it with Graphene-SGX, and successfully protect unmodified Memcached and SQLite with negligible overheads. The generated vulnerability checker detects novel vulnerabilities in the Graphene-SGX protection layer and production applications.
△ Less
Submitted 14 November, 2022;
originally announced November 2022.
-
A readahead prefetcher for GPU file system layer
Authors:
Vasilis Dimitsas,
Mark Silberstein
Abstract:
GPUs are broadly used in I/O-intensive big data applications. Prior works demonstrate the benefits of using GPU-side file system layer, GPUfs, to improve the GPU performance and programmability in such workloads. However, GPUfs fails to provide high performance for a common I/O pattern where a GPU is used to process a whole data set sequentially. In this work, we propose a number of system-level o…
▽ More
GPUs are broadly used in I/O-intensive big data applications. Prior works demonstrate the benefits of using GPU-side file system layer, GPUfs, to improve the GPU performance and programmability in such workloads. However, GPUfs fails to provide high performance for a common I/O pattern where a GPU is used to process a whole data set sequentially. In this work, we propose a number of system-level optimizations to improve the performance of GPUfs for such workloads. We perform an in-depth analysis of the interplay between the GPU I/O access pattern, CPU-GPU PCIe transfers and SSD storage, and identify the main bottlenecks. We propose a new GPU I/O readahead prefetcher and a GPU page cache replacement mechanism to resolve them. The GPU I/O readahead prefetcher achieves more than $2\times$ (geometric mean) higher bandwidth in a series of microbenchmarks compared to the original GPUfs. Furthermore, we evaluate the system on 14 applications derived from the RODINIA, PARBOIL and POLYBENCH benchmark suites. Our prefetching mechanism improves their execution time by up to 50% and their I/O bandwidth by 82% compared to the traditional CPU-only data transfer techniques.
△ Less
Submitted 11 September, 2021;
originally announced September 2021.
-
Revizor: Testing Black-box CPUs against Speculation Contracts
Authors:
Oleksii Oleksenko,
Christof Fetzer,
Boris Köpf,
Mark Silberstein
Abstract:
Speculative vulnerabilities such as Spectre and Meltdown expose speculative execution state that can be exploited to leak information across security domains via side-channels. Such vulnerabilities often stay undetected for a long time as we lack the tools for systematic testing of CPUs to find them.
In this paper, we propose an approach to automatically detect microarchitectural information lea…
▽ More
Speculative vulnerabilities such as Spectre and Meltdown expose speculative execution state that can be exploited to leak information across security domains via side-channels. Such vulnerabilities often stay undetected for a long time as we lack the tools for systematic testing of CPUs to find them.
In this paper, we propose an approach to automatically detect microarchitectural information leakage in commercial black-box CPUs. We build on speculation contracts, which we employ to specify the permitted side effects of program execution on the CPU's microarchitectural state. We propose a Model-based Relational Testing (MRT) technique to empirically assess the CPU compliance with these specifications.
We implement MRT in a testing framework called Revizor, and showcase its effectiveness on real Intel x86 CPUs. Revizor automatically detects violations of a rich set of contracts, or indicates their absence. A highlight of our findings is that Revizor managed to automatically surface Spectre, MDS, and LVI, as well as several previously unknown variants.
△ Less
Submitted 8 February, 2022; v1 submitted 14 May, 2021;
originally announced May 2021.
-
A Computational Approach to Packet Classification
Authors:
Alon Rashelbach,
Ori Rottenstreich,
Mark Silberstein
Abstract:
Multi-field packet classification is a crucial component in modern software-defined data center networks. To achieve high throughput and low latency, state-of-the-art algorithms strive to fit the rule lookup data structures into on-die caches; however, they do not scale well with the number of rules. We present a novel approach, NuevoMatch, which improves the memory scaling of existing methods. A…
▽ More
Multi-field packet classification is a crucial component in modern software-defined data center networks. To achieve high throughput and low latency, state-of-the-art algorithms strive to fit the rule lookup data structures into on-die caches; however, they do not scale well with the number of rules. We present a novel approach, NuevoMatch, which improves the memory scaling of existing methods. A new data structure, Range Query Recursive Model Index (RQ-RMI), is the key component that enables NuevoMatch to replace most of the accesses to main memory with model inference computations. We describe an efficient training algorithm that guarantees the correctness of the RQ-RMI-based classification. The use of RQ-RMI allows the rules to be compressed into model weights that fit into the hardware cache. Further, it takes advantage of the growing support for fast neural network processing in modern CPUs, such as wide vector instructions, achieving a rate of tens of nanoseconds per lookup. Our evaluation using 500K multi-field rules from the standard ClassBench benchmark shows a geometric mean compression factor of 4.9x, 8x, and 82x, and average performance improvement of 2.4x, 2.6x, and 1.6x in throughput compared to CutSplit, NeuroCuts, and TupleMerge, all state-of-the-art algorithms.
△ Less
Submitted 13 July, 2020; v1 submitted 10 February, 2020;
originally announced February 2020.
-
SpecFuzz: Bringing Spectre-type vulnerabilities to the surface
Authors:
Oleksii Oleksenko,
Bohdan Trach,
Mark Silberstein,
Christof Fetzer
Abstract:
SpecFuzz is the first tool that enables dynamic testing for speculative execution vulnerabilities (e.g., Spectre). The key is a novel concept of speculation exposure: The program is instrumented to simulate speculative execution in software by forcefully executing the code paths that could be triggered due to mispredictions, thereby making the speculative memory accesses visible to integrity check…
▽ More
SpecFuzz is the first tool that enables dynamic testing for speculative execution vulnerabilities (e.g., Spectre). The key is a novel concept of speculation exposure: The program is instrumented to simulate speculative execution in software by forcefully executing the code paths that could be triggered due to mispredictions, thereby making the speculative memory accesses visible to integrity checkers (e.g., AddressSanitizer). Combined with the conventional fuzzing techniques, speculation exposure enables more precise identification of potential vulnerabilities compared to state-of-the-art static analyzers.
Our prototype for detecting Spectre V1 vulnerabilities successfully identifies all known variations of Spectre V1 and decreases the mitigation overheads across the evaluated applications, reducing the amount of instrumented branches by up to 77% given a sufficient test coverage.
△ Less
Submitted 10 March, 2020; v1 submitted 24 May, 2019;
originally announced May 2019.
-
You Shall Not Bypass: Employing data dependencies to prevent Bounds Check Bypass
Authors:
Oleksii Oleksenko,
Bohdan Trach,
Tobias Reiher,
Mark Silberstein,
Christof Fetzer
Abstract:
A recent discovery of a new class of microarchitectural attacks called Spectre picked up the attention of the security community as these attacks can circumvent many traditional mechanisms of defense. One of the attacks---Bounds Check Bypass---can neither be efficiently solved on system nor architectural levels and requires changes in the application itself. So far, the proposed mitigations involv…
▽ More
A recent discovery of a new class of microarchitectural attacks called Spectre picked up the attention of the security community as these attacks can circumvent many traditional mechanisms of defense. One of the attacks---Bounds Check Bypass---can neither be efficiently solved on system nor architectural levels and requires changes in the application itself. So far, the proposed mitigations involved serialization, which reduces the usage of CPU resources and causes high overheads. In this report, we explore methods of delaying the vulnerable instructions without complete serialization. We discuss several ways of achieving it and compare them with Speculative Load Hardening, an existing solution based on a similar idea. The solutions of this type cause 60% overhead across Phoenix benchmark suite, which compares favorably to the full serialization causing 440% slowdown.
△ Less
Submitted 10 October, 2018; v1 submitted 22 May, 2018;
originally announced May 2018.
-
Faster Neural Network Training with Approximate Tensor Operations
Authors:
Menachem Adelman,
Kfir Y. Levy,
Ido Hakimi,
Mark Silberstein
Abstract:
We propose a novel technique for faster deep neural network training which systematically applies sample-based approximation to the constituent tensor operations, i.e., matrix multiplications and convolutions. We introduce new sampling techniques, study their theoretical properties, and prove that they provide the same convergence guarantees when applied to SGD training. We apply approximate tenso…
▽ More
We propose a novel technique for faster deep neural network training which systematically applies sample-based approximation to the constituent tensor operations, i.e., matrix multiplications and convolutions. We introduce new sampling techniques, study their theoretical properties, and prove that they provide the same convergence guarantees when applied to SGD training. We apply approximate tensor operations to single and multi-node training of MLP and CNN networks on MNIST, CIFAR-10 and ImageNet datasets. We demonstrate up to 66% reduction in the amount of computations and communication, and up to 1.37x faster training time while maintaining negligible or no impact on the final test accuracy.
△ Less
Submitted 25 October, 2021; v1 submitted 21 May, 2018;
originally announced May 2018.