Abstract Recent advances in machine learning have enabled Neural Network (NN) inference directly on constrained embedded devices. This local approach enhances the privacy of user data, as the inputs to the NN inference are not shared with third-party cloud providers over a communication network. At the same time, however, performing local NN inference on embedded devices opens up the possibility of Power Analysis attacks, which have recently been shown to be effective in recovering NN parameters, as well as their activations and structure. Knowledge of these NN characteristics constitutes a privacy threat, as it enables highly effective Membership Inference and Model Inversion attacks, which can recover information about the sensitive data that the NN model was trained on. In this paper we address the problem of securing sensitive NN inference parameters against Power Analysis attacks. Our approach employs masking, a countermeasure well-studied in the context of cryptographic algorithms. We design a set of gadgets, i.e., masked operations, tailored to NN inference. We prove our proposed gadgets secure against power attacks and show, both formally and experimentally, that they are composable, resulting in secure NN inference. We further propose optimizations that exploit intrinsic characteristics of NN inference to reduce the masking’s runtime and randomness requirements. We empirically evaluate the performance of our constructions, showing them to incur a slowdown by a factor of about 2–5.

This paper proposes to use intrinsic examples as a DNN fingerprinting technique for the functionality verification of DNN models implemented on edge devices. The proposed intrinsic examples do not affect the normal DNN training and can enable the black-box testing capability for DNN models packaged into edge device applications. We provide three algorithms for deriving intrinsic examples of the pre-trained model (the model before the DNN system design and implementation procedure) to retrieve the knowledge learnt from the training dataset for the detection of adversarial third-party attacks such as transfer learning and fault injection attack that may happen during the system implementation procedure. Besides, they can accommodate the model transformations due to various DNN model compression methods used by the system designer. quantization reduces redundancy in bit representation of weights [22, 26, 33]. With a k -bit weight representation, quantization maps weights into a total of 2 k quantized levels.

We consider the broad problem of analyzing safety properties of asynchronous concurrent programs under arbitrary thread interleavings. Delay-bounded deterministic scheduling , introduced in prior work, is an efficient bug-finding technique to curb the large cost associated with full scheduling nondeterminism. In this paper we first present a technique to lift the delay bound for the case of finite-domain variable programs, thus adding to the efficiency of bug detection the ability to prove safety of programs under arbitrary thread interleavings. Second, we demonstrate how, combined with predicate abstraction, our technique can both refute and verify safety properties of programs with unbounded variable domains, even for unbounded thread counts. Previous work has established that, for non-trivial concurrency routines, predicate abstraction induces a highly complex abstract program semantics. Our technique, however, never statically constructs an abstract parametric program; it only requires some abstract-states set to be closed under certain actions, thus eliminating the dependence on the existence of verification algorithms for abstract programs. We demonstrate the efficiency of our technique on many examples used in prior work, and showcase its simplicity compared to earlier approaches on the unbounded-thread Ticket Lock protocol.

We consider the broad problem of analyzing safety properties of asynchronous concurrent programs under arbitrary thread interleavings. Delay-bounded deterministic scheduling, introduced in prior work, is an efficient bug-finding technique to curb the large cost associated with full scheduling nondeterminism. In this paper we first present a technique to lift the delay bound for the case of finite-domain variable programs, thus adding to the efficiency of bug detection the ability to prove safety of programs under arbitrary thread interleavings. Second, we demonstrate how, combined with predicate abstraction, our technique can both refute and verify safety properties of programs with unbounded variable domains, even for unbounded thread counts. Previous work has established that, for non-trivial concurrency routines, predicate abstraction induces a highly complex abstract program semantics. Our technique, however, never statically constructs an abstract parametric program; it only requires some abstract-states set to be closed under certain actions, thus eliminating the dependence on the existence of verification algorithms for abstract programs. We demonstrate the efficiency of our technique on many examples used in prior work, and showcase its simplicity compared to earlier approaches on the unbounded-thread Ticket Lock protocol.

Neural Networks are used today in numerous security- and safety-relevant domains and are, as such, a popular target of attacks that subvert their classification capabilities, by manipulating the network parameters. Prior work has introduced sensitive samples-inputs highly sensitive to parameter changes-to detect such manipulations, and proposed a gradient ascent-based approach to compute them. In this paper we offer an alternative, using symbolic constraint solvers. We model the network and a formal specification of a sensitive sample in the language of the solver and ask for a solution. This approach supports a rich class of queries, corresponding, for instance, to the presence of certain types of attacks. Unlike earlier techniques, our approach does not depend on convex search domains, or on the suitability of a starting point for the search. We address the performance limitations of constraint solvers by partitioning the search space for the solver, and exploring the partitions according to a balanced schedule that still retains completeness of the search. We demonstrate the impact of the use of solvers in terms of functionality and search efficiency, using a case study for the detection of Trojan attacks on Neural Networks.

A classical result by Ramalingam about synchronization-sensitive interprocedural program analysis implies that reachability for concurrent threads running recursive procedures is undecidable. A technique proposed by Qadeer and Rehof, to bound the number of context switches allowed between the threads, leads to an incomplete solution that is, however, believed to catch “most bugs” in practice, as errors tend to occur within few contexts. The question of whether the technique can also prove the absence of bugs at least in some cases has remained largely open. Toward closing this gap, we introduce in this article the generic verification paradigm of observation sequences for resource-parameterized programs. Such a sequence observes how increasing the resource parameter affects the reachability of states satisfying a given property. The goal is to show that increases beyond some “cutoff” parameter value have no impact on the reachability—the sequence has converged. This allows us to conclude that the property holds for all parameter values. We applied this paradigm to the context-unbounded program analysis problem, choosing the resource to be the number of permitted thread context switches. The result is a partially correct interprocedural reachability analysis technique for concurrent shared-memory programs. Our technique may not terminate but is able to both refute and prove context-unbounded safety for such programs. We demonstrate the effectiveness and efficiency of the technique using a variety of benchmark programs. The safe instances cannot be proved safe by earlier, context-bounded methods.

The effectiveness of masking as a countermeasure against information leakage in cryptographic ciphers is contingent upon individual instructions leaking information independently. An example of dependent leakage is transitionbased leakage: side-channels can leak data proportional to the exclusive-or of the old and the new value during a register write, despite proper first-order masking. In this paper we present a technique to detect and repair transition-based leakage. Our detection technique symbolically executes a binary to relate the old and new values during a register write. We then combine existing analyses to check for, and quantify, any leakage caused by the write. Our repair module closes a leak by flushing the affected register before writing it. We also present a fully automated detection and repair tool called BATTL, which is the first to our knowledge to operate at the binary level and is thus sensitive to decisions at any compilation stage that may affect security. We evaluate BATTL against first-order secure implementations of the AES block cipher, and of a secure multiplicative inversion algorithm. BATTL identified a number of transition-based leakages, some with high leakage amounts. Our countermeasure removes all first-order leakages with only moderate runtime overhead.

Trained Deep Neural Network (DNN) models have become valuable intellectual property. A new attack surface has emerged for DNNs: model reverse engineering. Several recent attempts have utilized various common side channels. However, recovering DNN parameters, weights and biases, remains a challenge. In this paper, we present a novel attack that utilizes a floating-point timing side channel to reverse-engineer parameters of multi-layer perceptron (MLP) models in software implementation, entirely and precisely. To the best of our knowledge, this is the first work that leverages a floating-point timing side-channel for effective DNN model recovery.

Recent years have seen various side-channel timing attacks demonstrated on both CPUs and GPUs, in diverse settings such as desktops, clouds, and mobile systems. These attacks observe events on different shared resources on the memory hierarchy from timing information, and then infer secret-dependent memory access pattern to retrieve the secret through statistical analysis. We generalize these attacks as memory-based side-channel attacks. In this paper, we propose a novel software countermeasure, MemPoline, against memory-based side-channel attacks. MemPoline hides the secretdependent memory access pattern by moving sensitive data around randomly within a memory space. Compared to the prior oblivious RAM technology, MemPoline employs parameter-directed permutations to achieve randomness, which are significantly more efficient and yet provide similar security. Our countermeasure only requires modifying the source code, and has great advantages of being general algorithm-agnostic, portable independent of the underlying architecture, and compatible a userspace approach that works for any operating system or hypervisor. We run a thorough evaluation of our countermeasure. We apply it to both AES, a symmetric cipher, and RSA, an asymmetric cipher. Both empirical results and theoretical analysis show that our countermeasure resists a series of existing memory-based side-channel attacks on CPUs and GPUs.

Security of deep neural network (DNN) inference engines, i.e., trained DNN models on various platforms, has become one of the biggest challenges in deploying artificial intelligence in domains where privacy, safety, and reliability are of paramount importance, such as in medical applications. In addition to classic software attacks such as model inversion and evasion attacks, recently a new attack surface-implementation attacks which include both passive side-channel attacks and active fault injection and adversarial attacks-is arising, targeting implementation peculiarities of DNN to breach their confidentiality and integrity. This paper presents several novel passive and active attacks on DNN we have developed and tested over medical datasets. Our new attacks reveal a largely under-explored attack surface of DNN inference engines. Insights gained during attack exploration will provide valuable guidance for effectively protecting DNN execution against reverse-engineering and integrity violations.

The results of numerical computations with floating point numbers depend on the execution platform, which we define as the hardware and the tools (compilers, etc.) supporting that hardware. One reason for the dependence is that compilers have significant freedom in deciding how to evaluate a floating point expression, as such evaluation is not standardized (not even in standards such as IEEE-754). Another reason is that hardware may or may not provide specialized instructions like Fused Multiply Add (FMA), and if it does, the compiler can take advantage of FMA functionality in different ways. We call an expression volatile if, for some input, its value differs across platform parameters. Differences can become particularly large across heterogeneous parallel architectures. This undermines the software portability promised by programming standards such as OpenCL and significantly impacts reproducibility of results in general. In this paper, we present a technique that predicts bounds on the output of a program containing volatile expressions when executed on different platforms. Using randomly selected inputs, we compare the bounds to results from running the code across a variety of platforms including CPUs and GPUs. Our results show that the theoretical bounds are relatively tight (within an order of magnitude) and can help users pinpoint where results should be stabilized, for instance by restricting expression reordering.

We address the problem of analyzing asynchronous event-driven programs, in which concurrent agents communicate via unbounded message queues. The safety verification problem for such programs is undecidable. We present in this paper a technique that combines queue-bounded exploration with a convergence test: if the sequence of certain abstractions of the reachable states, for increasing queue bounds k, converges, we can prove any property of the program that is preserved by the abstraction. If the abstract state space is finite, convergence is guaranteed; the challenge is to catch the point k_max where it happens. We further demonstrate how simple invariants formulated over the concrete domain can be used to eliminate spurious abstract states, which otherwise prevent the sequence from converging. We have implemented our technique for the P programming language for event-driven programs. We show experimentally that the sequence of abstractions often converges fully automatically, in hard cases with minimal designer support in the form of sequentially provable invariants, and that this happens for a value of k_max small enough to allow the method to succeed in practice.

A classical result by Ramalingam about synchronization-sensitive interprocedural program analysis implies that reachability for concurrent threads running recursive procedures is undecidable. A technique proposed by Qadeer and Rehof, to bound the number of context switches allowed between the threads, leads to an incomplete solution that is, however, believed to catch "most bugs" in practice. The question whether the technique can also prove the absence of bugs at least in some cases has remained largely open. In this paper we introduce a broad verification methodology for resource-parameterized programs that observes how changes to the resource parameter affect the behavior of the program. Applied to the context-unbounded analysis problem (CUBA), the methodology results in partial verification techniques for procedural concurrent programs. Our solutions may not terminate, but are able to both refute and prove context-unbounded safety for concurrent recursive threads. We demonstrate the effectiveness of our method using a variety of examples, the safe of which cannot be proved safe by earlier, context-bounded methods.

As the new hash standard, Keccak-based secure hash function (SHA-3) will be used in various cryptographic applications. Its security will be of paramount importance to the systems built on top of it. This paper proposes efficient algebraic fault analysis (AFA) methods, and for the first time, applies them to all four modes of SHA-3 under relaxed fault models. Our AFA utilizes the clear algebraic properties of Keccak operations and is very suitable for the fault analysis of SHA-3. Both our analysis and experimental results show that the proposed AFA method is more efficient than the traditional differential fault analysis (DFA) under the single-byte fault model, requiring much fewer faults to recover a whole internal state of the hashing computation. Meanwhile, as AFA is able to exploit all the information available, it can be applied to SHA-3 modes with shorter digests and under more relaxed fault models, where often times the DFA method fails. Our results show that AFA can successfully break all the four SHA-3 modes under a 16-bit fault model, and break SHA3-512 under an even more relaxed fault model, 32-bit fault, all within several minutes. The successful AFA on SHA-3 demonstrates the vulnerability of Keccak algorithms to fault analysis, calling for protections against fault injection and fault analysis.

Microarchitectural side-channel attacks have posed serious threats to many computing systems, ranging from embedded systems and mobile devices to desktop workstations and cloud servers. Such attacks exploit side-channel vulnerabilities stemming from fundamental microarchitectural performance features, including the most common caches, out-of-order execution (for the newly revealed Meltdown exploit), and speculative execution (for Spectre). Prior efforts have focused on identifying and assessing these security vulnerabilities, and designing and implementing countermeasures against them. However, the efforts aiming at detecting specific side-channel attacks tend to be narrowly focused, which can make them effective but also makes them obsolete very quickly. In this paper, we propose a new methodology for detecting microarchitectural side-channel attacks that has the potential for a wide scope of applicability, as we demonstrate using a case study involving the Prime+Probe attack family. Instead of looking at the side-effects of side-channel attacks on microarchitectural elements such as hardware performance counters, we target the high-level semantics and invariant patterns of these attacks. We have applied our method to different Prime+Probe attack variants on the instruction cache, data cache, and last-level cache, as well as several benign programs as benchmarks. The method can detect all of the Prime+Probe attack variants with a true positive rate of 100% and an average false positive rate of 7.4%.

Floating-point arithmetic is a loosely standardized approximation of real arithmetic available on many computers today. Architectural and compiler differences can lead to diverse calculations across platforms, for the same input. If left untreated, platform dependence, called volatility in this paper, seriously interferes with result reproducibility and, ultimately, program portability. We present an approach to stabilizing floating-point programs against volatility. Our approach, dubbed provenance analysis, traces volatility observed in a given intermediate expression E back to volatility in preceding statements, and quantifies individual contributions to the volatility in E. Statements contributing the most are then stabilized, by disambiguating the arithmetic using expression rewriting and control pragmas. The benefit of local (as opposed to program-wide) stabilization is that compilers are free to engage performance- or precision-enhancing optimizations across program fragments that do not destabilize E. We have implemented our technique in a dynamic analysis tool that reports both volatility and provenance information. We demonstrate that local program stabilization often suffices to reduce platform dependence to an acceptable level.

This paper presents an efficient algebraic fault analysis on all four modes of SHA-3 under relaxed fault models. This is the first work to apply algebraic techniques on fault analysis of SHA-3. Results show that algebraic fault analysis on SHA-3 is very efficient and effective due to the clear algebraic properties of Keccak operations. Comparing with previous work on differential fault analysis of SHA-3, algebraic fault analysis can identify the injected faults with much higher rates, and recover an entire internal state of the penultimate round with much fewer fault injections.

Side-channel attack utilizes side-channel leakages to extract the secret in crypto systems. Various countermeasures for different algorithms and platforms have been proposed to protect crypto systems against such attacks. Manual countermeasure design requires deep understanding of the target algorithm and implementation, and oftentimes is platform-specific and error-prone. In this paper, we propose the construction of Threshold Implementation (TI), a provably secure countermeasure against power attacks, as an automated compiler pass in the open LLVM (Low Level Virtual Machine) framework. Attack results show that the automatically generated TI designs are secure against power attacks. As our proposed scheme implements the countermeasure at the intermediate representation (IR) level, our method can be applied to any cipher software in any programming language, and the generated implementations can be ported to different platforms and architectures.

Exploration algorithms for explicit-state transition systems are a core back-end technology in program verification. They can be applied to programs by generating the transition system on the fly, avoiding an expensive up-front translation. An on-the-fly strategy requires significant modifications to the implementation, into a form that stores states directly as valuations of program variables. Performed manually on a per-algorithm basis, such modifications are laborious and error-prone. In this paper we present the IJIT Application Programming Interface (API), which allows users to automatically transform a given transition system exploration algorithm to one that operates on Boolean programs. The API converts system states temporarily to program states just in time for expansion via image computations, forward or backward. Using our API, we have effortlessly extended various non-trivial (e.g. infinite-state) model checking algorithms to operate on multi-threaded Boolean programs. We demonstrate the ease of use of the API, and present a case study on the impact of the just-in-time translation on these algorithms.

Precise reasoning for floating-point arithmetic (FPA) is as critical for accurate software analysis as it is hard to achieve. Several recent approaches reduce solving an FPA formula f to reasoning over a related but easier-to-solve proxy theory. The rationale is that a satisfying proxy assignment may directly correspond to a model for f. But what if it doesn't? Prior work deals with this case somewhat crudely, or discards the proxy assignment altogether. In this paper we present an FPA decision framework, parameterized by the choice of proxy theory T, that attempts to lift an encountered T model to a numerically close FPA model. Other than assuming some "proximity" of T to FPA, our lifting procedure is T-agnostic; it is in fact designed to work independently of how the proxy assignment was obtained. Should the lifting fail, our procedure gradually reduces the gap between the FPA and the proxy interpretations of f. We have instantiated the framework using real arithmetic and reduced-precision FPA as proxy theories, and demonstrate that we can, in many cases, decide f more efficiently than earlier work.