• ### Formal Security Analysis of Neural Networks using Symbolic Intervals(1804.10829)

April 28, 2018 cs.LO, cs.AI
Due to the increasing deployment of Deep Neural Networks (DNNs) in real-world security-critical domains including autonomous vehicles and collision avoidance systems, formally checking security properties of DNNs, especially under different attacker capabilities, is becoming crucial. Most existing security testing techniques for DNNs try to find adversarial examples without providing any formal security guarantees about the non-existence of adversarial examples. Recently, several projects have used different types of Satisfiability Modulo Theory (SMT) solvers to formally check security properties of DNNs. However, all of these approaches are limited by the high overhead caused by the solver. In this paper, we present a new direction for formally checking security properties of DNNs without using SMT solvers. Instead, we leverage interval arithmetic to formally check security properties by computing rigorous bounds on the DNN outputs. Our approach, unlike existing solver-based approaches, is easily parallelizable. We further present symbolic interval analysis along with several other optimizations to minimize overestimations. We design, implement, and evaluate our approach as part of ReluVal, a system for formally checking security properties of Relu-based DNNs. Our extensive empirical results show that ReluVal outperforms Reluplex, a state-of-the-art solver-based system, by 200 times on average for the same security properties. ReluVal is able to prove a security property within 4 hours on a single 8-core machine without GPUs, while Reluplex deemed inconclusive due to timeout (more than 5 days). Our experiments demonstrate that symbolic interval analysis is a promising new direction towards rigorously analyzing different security properties of DNNs.
• ### DeepXplore: Automated Whitebox Testing of Deep Learning Systems(1705.06640)

Sept. 24, 2017 cs.CR, cs.SE, cs.LG
Deep learning (DL) systems are increasingly deployed in safety- and security-critical domains including self-driving cars and malware detection, where the correctness and predictability of a system's behavior for corner case inputs are of great importance. Existing DL testing depends heavily on manually labeled data and therefore often fails to expose erroneous behaviors for rare inputs. We design, implement, and evaluate DeepXplore, the first whitebox framework for systematically testing real-world DL systems. First, we introduce neuron coverage for systematically measuring the parts of a DL system exercised by test inputs. Next, we leverage multiple DL systems with similar functionality as cross-referencing oracles to avoid manual checking. Finally, we demonstrate how finding inputs for DL systems that both trigger many differential behaviors and achieve high neuron coverage can be represented as a joint optimization problem and solved efficiently using gradient-based search techniques. DeepXplore efficiently finds thousands of incorrect corner case behaviors (e.g., self-driving cars crashing into guard rails and malware masquerading as benign software) in state-of-the-art DL models with thousands of neurons trained on five popular datasets including ImageNet and Udacity self-driving challenge data. For all tested DL models, on average, DeepXplore generated one test input demonstrating incorrect behavior within one second while running only on a commodity laptop. We further show that the test inputs generated by DeepXplore can also be used to retrain the corresponding DL model to improve the model's accuracy by up to 3%.
• Substantial experimental and theoretical efforts worldwide are devoted to explore the phase diagram of strongly interacting matter. At LHC and top RHIC energies, QCD matter is studied at very high temperatures and nearly vanishing net-baryon densities. There is evidence that a Quark-Gluon-Plasma (QGP) was created at experiments at RHIC and LHC. The transition from the QGP back to the hadron gas is found to be a smooth cross over. For larger net-baryon densities and lower temperatures, it is expected that the QCD phase diagram exhibits a rich structure, such as a first-order phase transition between hadronic and partonic matter which terminates in a critical point, or exotic phases like quarkyonic matter. The discovery of these landmarks would be a breakthrough in our understanding of the strong interaction and is therefore in the focus of various high-energy heavy-ion research programs. The Compressed Baryonic Matter (CBM) experiment at FAIR will play a unique role in the exploration of the QCD phase diagram in the region of high net-baryon densities, because it is designed to run at unprecedented interaction rates. High-rate operation is the key prerequisite for high-precision measurements of multi-differential observables and of rare diagnostic probes which are sensitive to the dense phase of the nuclear fireball. The goal of the CBM experiment at SIS100 (sqrt(s_NN) = 2.7 - 4.9 GeV) is to discover fundamental properties of QCD matter: the phase structure at large baryon-chemical potentials (mu_B > 500 MeV), effects of chiral symmetry, and the equation-of-state at high density as it is expected to occur in the core of neutron stars. In this article, we review the motivation for and the physics programme of CBM, including activities before the start of data taking in 2022, in the context of the worldwide efforts to explore high-density QCD matter.
• ### FIRED: Frequent Inertial Resets with Diversification for Emerging Commodity Cyber-Physical Systems(1702.06595)

Feb. 21, 2017 cs.CR, cs.SY
A Cyber-Physical System (CPS) is defined by its unique characteristics involving both the cyber and physical domains. Their hybrid nature introduces new attack vectors, but also provides an opportunity to design new security defenses. In this paper, we present a new domain-specific security mechanism, FIRED, that leverages physical properties such as inertia of the CPS to improve security. FIRED is simple to describe and implement. It goes through two operations: Reset and Diversify, as frequently as possible -- typically in the order of seconds or milliseconds. The combined effect of these operations is that attackers are unable to gain persistent control of the system. The CPS stays safe and stable even under frequent resets because of the inertia present. Further, resets simplify certain diversification mechanisms and makes them feasible to implement in CPSs with limited computing resources. We evaluate our idea on two real-world systems: an engine management unit of a car and a flight controller of a quadcopter. Roughly speaking, these two systems provide typical and extreme operational requirements for evaluating FIRED in terms of stability, algorithmic complexity, and safety requirements. We show that FIRED provides robust security guarantees against hijacking attacks and persistent CPS threats. We find that our defense is suitable for emerging CPS such as commodity unmanned vehicles that are currently unregulated and cost sensitive.
• ### Applications of gauge duality in robust principal component analysis and semidefinite programming(1601.06893)

May 9, 2016 math.OC
Gauge duality theory was originated by Freund [Math. Programming, 38(1):47-67, 1987] and was recently further investigated by Friedlander, Mac{\^e}do and Pong [SIAM J. Optm., 24(4):1999-2022, 2014]. When solving some matrix optimization problems via gauge dual, one is usually able to avoid full matrix decompositions such as singular value and/or eigenvalue decompositions. In such an approach, a gauge dual problem is solved in the first stage, and then an optimal solution to the primal problem can be recovered from the dual optimal solution obtained in the first stage. Recently, this theory has been applied to a class of \emph{semidefinite programming} (SDP) problems with promising numerical results [Friedlander and Mac{\^e}do, SIAM J. Sci. Comp., to appear, 2016]. In this paper, we establish some theoretical results on applying the gauge duality theory to robust \emph{principal component analysis} (PCA) and general SDP. For each problem, we present its gauge dual problem, characterize the optimality conditions for the primal-dual gauge pair, and validate a way to recover a primal optimal solution from a dual one. These results are extensions of [Friedlander and Mac{\^e}do, SIAM J. Sci. Comp., to appear, 2016] from nuclear norm regularization to robust PCA and from a special class of SDP which requires the coefficient matrix in the linear objective to be positive definite to SDP problems without this restriction. Our results provide further understanding in the potential advantages and disadvantages of the gauge duality theory.
• ### EOS: Automatic In-vivo Evolution of Kernel Policies for Better Performance(1508.06356)

Oct. 18, 2015 cs.OS
Today's monolithic kernels often implement a small, fixed set of policies such as disk I/O scheduling policies, while exposing many parameters to let users select a policy or adjust the specific setting of the policy. Ideally, the parameters exposed should be flexible enough for users to tune for good performance, but in practice, users lack domain knowledge of the parameters and are often stuck with bad, default parameter settings. We present EOS, a system that bridges the knowledge gap between kernel developers and users by automatically evolving the policies and parameters in vivo on users' real, production workloads. It provides a simple policy specification API for kernel developers to programmatically describe how the policies and parameters should be tuned, a policy cache to make in-vivo tuning easy and fast by memorizing good parameter settings for past workloads, and a hierarchical search engine to effectively search the parameter space. Evaluation of EOS on four main Linux subsystems shows that it is easy to use and effectively improves each subsystem's performance.
• ### Inertial primal-dual algorithms for structured convex optimization(1409.2992)

Sept. 10, 2014 math.OC
The primal-dual algorithm recently proposed by Chambolle & Pock (abbreviated as CPA) for structured convex optimization is very efficient and popular. It was shown by Chambolle & Pock in \cite{CP11} and also by Shefi & Teboulle in \cite{ST14} that CPA and variants are closely related to preconditioned versions of the popular alternating direction method of multipliers (abbreviated as ADM). In this paper, we further clarify this connection and show that CPAs generate exactly the same sequence of points with the so-called linearized ADM (abbreviated as LADM) applied to either the primal problem or its Lagrangian dual, depending on different updating orders of the primal and the dual variables in CPAs, as long as the initial points for the LADM are properly chosen. The dependence on initial points for LADM can be relaxed by focusing on cyclically equivalent forms of the algorithms. Furthermore, by utilizing the fact that CPAs are applications of a general weighted proximal point method to the mixed variational inequality formulation of the KKT system, where the weighting matrix is positive definite under a parameter condition, we are able to propose and analyze inertial variants of CPAs. Under certain conditions, global point-convergence, nonasymptotic $O(1/k)$ and asymptotic $o(1/k)$ convergence rate of the proposed inertial CPAs can be guaranteed, where $k$ denotes the iteration index. Finally, we demonstrate the profits gained by introducing the inertial extrapolation step via experimental results on compressive image reconstruction based on total variation minimization.
• ### A general inertial proximal point method for mixed variational inequality problem(1407.8238)

Aug. 1, 2014 math.OC
In this paper, we first propose a general inertial proximal point method for the mixed variational inequality (VI) problem. Based on our knowledge, without stronger assumptions, convergence rate result is not known in the literature for inertial type proximal point methods. Under certain conditions, we are able to establish the global convergence and a $o(1/k)$ convergence rate result (under certain measure) of the proposed general inertial proximal point method. We then show that the linearized alternating direction method of multipliers (ADMM) for separable convex optimization with linear constraints is an application of a general proximal point method, provided that the algorithmic parameters are properly chosen. As byproducts of this finding, we establish global convergence and $O(1/k)$ convergence rate results of the linearized ADMM in both ergodic and nonergodic sense. In particular, by applying the proposed inertial proximal point method for mixed VI to linearly constrained separable convex optimization, we obtain an inertial version of the linearized ADMM for which the global convergence is guaranteed. We also demonstrate the effect of the inertial extrapolation step via experimental results on the compressive principal component pursuit problem.
• ### A Fast Algorithm for Total Variation Image Reconstruction from Random Projections(1001.1774)

Jan. 12, 2010 math.OC
Total variation (TV) regularization is popular in image restoration and reconstruction due to its ability to preserve image edges. To date, most research activities on TV models concentrate on image restoration from blurry and noisy observations, while discussions on image reconstruction from random projections are relatively fewer. In this paper, we propose, analyze, and test a fast alternating minimization algorithm for image reconstruction from random projections via solving a TV regularized least-squares problem. The per-iteration cost of the proposed algorithm involves a linear time shrinkage operation, two matrix-vector multiplications and two fast Fourier transforms. Convergence, certain finite convergence and $q$-linear convergence results are established, which indicate that the asymptotic convergence speed of the proposed algorithm depends on the spectral radii of certain submatrix. Moreover, to speed up convergence and enhance robustness, we suggest an accelerated scheme based on an inexact alternating direction method. We present experimental results to compare with an existing algorithm, which indicate that the proposed algorithm is stable, efficient and competitive with TwIST \cite{TWIST} -- a state-of-the art algorithm for solving TV regularization problems.
• ### Alternating Direction Algorithms for $\ell_1$-Problems in Compressive Sensing(0912.1185)

Dec. 7, 2009 math.OC
In this paper, we propose and study the use of alternating direction algorithms for several $\ell_1$-norm minimization problems arising from sparse solution recovery in compressive sensing, including the basis pursuit problem, the basis-pursuit denoising problems of both unconstrained and constrained forms, as well as others. We present and investigate two classes of algorithms derived from either the primal or the dual forms of the $\ell_1$-problems. The construction of the algorithms consists of two main steps: (1) to reformulate an $\ell_1$-problem into one having partially separable objective functions by adding new variables and constraints; and (2) to apply an exact or inexact alternating direction method to the resulting problem. The derived alternating direction algorithms can be regarded as first-order primal-dual algorithms because both primal and dual variables are updated at each and every iteration. Convergence properties of these algorithms are established or restated when they already exist. Extensive numerical results in comparison with several state-of-the-art algorithms are given to demonstrate that the proposed algorithms are efficient, stable and robust. Moreover, we present numerical results to emphasize two practically important but perhaps overlooked points. One point is that algorithm speed should always be evaluated relative to appropriate solution accuracy; another is that whenever erroneous measurements possibly exist, the $\ell_1$-norm fidelity should be the fidelity of choice in compressive sensing.