Computer Science Department Technical Reports
http://hdl.handle.net/1903/2225
2015-08-23T08:20:39ZChecking Interaction-Based Declassification Policies for Android Using Symbolic Execution
http://hdl.handle.net/1903/16756
Checking Interaction-Based Declassification Policies for Android Using Symbolic Execution
Micinski, Kristopher; Fetter-Degges, Jonathan; Jeon, Jinseong; Foster, Jeffrey S.; Clarkson, Michael R.
Mobile apps can access a wide variety of secure information, such as contacts and location. However, current mobile platforms include only coarse access control mechanisms to protect such data. In this paper, we introduce interaction-based declassification policies, in which the user's interactions with the app constrain the release of
sensitive information. Our policies are defined extensionally, so as to be independent of the app's implementation, based on sequences of security-relevant events that occur in app runs. Policies use LTL formulae to precisely specify which secret inputs, read at which times, may be released. We formalize a semantic security condition, interaction-based noninterference, to define our policies precisely. Finally, we describe a prototype tool that uses symbolic execution of Dalvik bytecode to check interaction-based declassification policies for Android, and we show that it enforces policies correctly on a set of apps.
2015-07-01T00:00:00ZAccurate computation of Galerkin double surface integrals in the 3-D boundary element method
http://hdl.handle.net/1903/16394
Accurate computation of Galerkin double surface integrals in the 3-D boundary element method
Adelman, Ross; Gumerov, Nail A.; Duraiswami, Ramani
Many boundary element integral equation kernels are based on the Green’s functions of the Laplace and Helmholtz equations in three dimensions. These include, for example, the Laplace, Helmholtz, elasticity, Stokes, and Maxwell equations. Integral equation formulations lead to more compact, but dense linear systems. These dense systems are often solved iteratively via Krylov subspace methods, which may be accelerated via the fast multipole method. There are advantages to Galerkin formulations for such integral equations, as they treat problems associated with kernel singularity, and lead to symmetric and better conditioned matrices. However, the Galerkin method requires each entry in the system matrix to be created via the computation of a double surface integral over one or more pairs of triangles. There are a number of semi-analytical methods to treat these integrals, which all have some issues, and are discussed in this paper. We present novel methods to compute all the integrals that arise in Galerkin formulations involving kernels based on the Laplace and Helmholtz Green’s functions to any specified accuracy. Integrals involving completely geometrically separated triangles are non-singular and are computed using a technique based on spherical harmonics and multipole expansions and translations, which results in the integration of polynomial functions over the triangles.
Integrals involving cases where the triangles have common vertices, edges, or are coincident are treated via scaling and symmetry arguments, combined with automatic recursive geometric decomposition of the integrals. Example results are presented, and the developed software is available as open source.
2015-05-29T00:00:00ZAutomating Efficient RAM-Model Secure Computation
http://hdl.handle.net/1903/15552
Automating Efficient RAM-Model Secure Computation
Liu, Chang; Huang, Yan; Shi, Elaine; Katz, Jonathan; Hicks, Michael
RAM-model secure computation addresses the inherent limitations of
circuit-model secure computation considered in almost all previous work.
Here, we describe the first automated approach for RAM-model secure
computation in the semi-honest model. We define an intermediate
representation called SCVM and a corresponding type system suited for
RAM-model secure computation. Leveraging compile-time optimizations, our
approach achieves order-of-magnitude speedups compared to both
circuit-model secure computation and the state-of-art RAM-model secure
computation.
2014-03-13T00:00:00ZA Stochastic Approach to Uncertainty in the Equations of MHD Kinematics
http://hdl.handle.net/1903/15523
A Stochastic Approach to Uncertainty in the Equations of MHD Kinematics
Phillips, Edward G.; Elman, Howard C.
The magnetohydodynamic (MHD) kinematics model describes the
electromagnetic behavior of an electrically conducting fluid when its
hydrodynamic properties are assumed to be known. In particular, the MHD
kinematics equations can be used to simulate the magnetic field induced
by a given velocity field. While prescribing the velocity field leads to
a simpler model than the fully coupled MHD system, this may introduce
some epistemic uncertainty into the model. If the velocity of a physical
system is not known with certainty, the magnetic field obtained from the
model may not be reflective of the magnetic field seen in experiments.
Additionally, uncertainty in physical parameters such as the magnetic
resistivity may affect the reliability of predictions obtained from this
model. By modeling the velocity and the resistivity as random variables
in the MHD kinematics model, we seek to quantify the effects of
uncertainty in these fields on the induced magnetic field. We develop
stochastic expressions for these quantities and investigate their impact
within a finite element discretization of the kinematics equations. We
obtain mean and variance data through Monte-Carlo simulation for several
test problems. Toward this end, we develop and test an efficient block
preconditioner for the linear systems arising from the discretized
equations.
2014-07-10T00:00:00Z