
Due to the increasing deployment of Deep Neural Networks (DNNs) in realworld
securitycritical 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 nonexistence 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 solverbased 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 Relubased DNNs. Our extensive
empirical results show that ReluVal outperforms Reluplex, a stateoftheart
solverbased 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 8core
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.

Deep learning (DL) systems are increasingly deployed in safety and
securitycritical domains including selfdriving 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 realworld 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 crossreferencing 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 gradientbased search techniques.
DeepXplore efficiently finds thousands of incorrect corner case behaviors
(e.g., selfdriving cars crashing into guard rails and malware masquerading as
benign software) in stateoftheart DL models with thousands of neurons
trained on five popular datasets including ImageNet and Udacity selfdriving
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
netbaryon densities. There is evidence that a QuarkGluonPlasma (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 netbaryon densities
and lower temperatures, it is expected that the QCD phase diagram exhibits a
rich structure, such as a firstorder 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 highenergy heavyion 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 netbaryon densities, because it is
designed to run at unprecedented interaction rates. Highrate operation is the
key prerequisite for highprecision measurements of multidifferential
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 baryonchemical potentials (mu_B > 500
MeV), effects of chiral symmetry, and the equationofstate 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 highdensity QCD matter.

A CyberPhysical 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 domainspecific 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 realworld 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.

Gauge duality theory was originated by Freund [Math. Programming,
38(1):4767, 1987] and was recently further investigated by Friedlander,
Mac{\^e}do and Pong [SIAM J. Optm., 24(4):19992022, 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 primaldual 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.

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 invivo 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.

The primaldual 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 socalled
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 pointconvergence, 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.

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.

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 leastsquares problem. The
periteration cost of the proposed algorithm involves a linear time shrinkage
operation, two matrixvector 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 stateofthe art algorithm for solving TV regularization
problems.

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 basispursuit 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 firstorder primaldual 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
stateoftheart 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.