-
Confidential Consortium Framework: Secure Multiparty Applications with Confidentiality, Integrity, and High Availability
Authors:
Heidi Howard,
Fritz Alder,
Edward Ashton,
Amaury Chamayou,
Sylvan Clebsch,
Manuel Costa,
Antoine Delignat-Lavaud,
Cedric Fournet,
Andrew Jeffery,
Matthew Kerner,
Fotios Kounelis,
Markus A. Kuppe,
Julien Maffre,
Mark Russinovich,
Christoph M. Wintersteiger
Abstract:
Confidentiality, integrity protection, and high availability, abbreviated to CIA, are essential properties for trustworthy data systems. The rise of cloud computing and the growing demand for multiparty applications however means that building modern CIA systems is more challenging than ever. In response, we present the Confidential Consortium Framework (CCF), a general-purpose foundation for deve…
▽ More
Confidentiality, integrity protection, and high availability, abbreviated to CIA, are essential properties for trustworthy data systems. The rise of cloud computing and the growing demand for multiparty applications however means that building modern CIA systems is more challenging than ever. In response, we present the Confidential Consortium Framework (CCF), a general-purpose foundation for develo** secure stateful CIA applications. CCF combines centralized compute with decentralized trust, supporting deployment on untrusted cloud infrastructure and transparent governance by mutually untrusted parties. CCF leverages hardware-based trusted execution environments for remotely verifiable confidentiality and code integrity. This is coupled with state machine replication backed by an auditable immutable ledger for data integrity and high availability. CCF enables each service to bring its own application logic, custom multiparty governance model, and deployment scenario, decoupling the operators of nodes from the consortium that governs them. CCF is open-source and available now at https://github.com/microsoft/CCF.
△ Less
Submitted 17 October, 2023;
originally announced October 2023.
-
Parma: Confidential Containers via Attested Execution Policies
Authors:
Matthew A. Johnson,
Stavros Volos,
Ken Gordon,
Sean T. Allen,
Christoph M. Wintersteiger,
Sylvan Clebsch,
John Starks,
Manuel Costa
Abstract:
Container-based technologies empower cloud tenants to develop highly portable software and deploy services in the cloud at a rapid pace. Cloud privacy, meanwhile, is important as a large number of container deployments operate on privacy-sensitive data, but challenging due to the increasing frequency and sophistication of attacks. State-of-the-art confidential container-based designs leverage proc…
▽ More
Container-based technologies empower cloud tenants to develop highly portable software and deploy services in the cloud at a rapid pace. Cloud privacy, meanwhile, is important as a large number of container deployments operate on privacy-sensitive data, but challenging due to the increasing frequency and sophistication of attacks. State-of-the-art confidential container-based designs leverage process-based trusted execution environments (TEEs), but face security and compatibility issues that limits their practical deployment. We propose Parma, an architecture that provides lift-and-shift deployment of unmodified containers while providing strong security protection against a powerful attacker who controls the untrusted host and hypervisor. Parma leverages VM-level isolation to execute a container group within a unique VM-based TEE. Besides container integrity and user data confidentiality and integrity, Parma also offers container attestation and execution integrity based on an attested execution policy. Parma execution policies provide an inductive proof over all future states of the container group. This proof, which is established during initialization, forms a root of trust that can be used for secure operations within the container group without requiring any modifications of the containerized workflow itself (aside from the inclusion of the execution policy.) We evaluate Parma on AMD SEV-SNP processors by running a diverse set of workloads demonstrating that workflows exhibit 0-26% additional overhead in performance over running outside the enclave, with a mean 13% overhead on SPEC2017, while requiring no modifications to their program code. Adding execution policies introduces less than 1% additional overhead. Furthermore, we have deployed Parma as the underlying technology driving Confidential Containers on Azure Container Instances.
△ Less
Submitted 7 March, 2023; v1 submitted 8 February, 2023;
originally announced February 2023.
-
Convergence analysis of some tent-based schemes for linear hyperbolic systems
Authors:
Dow Drake,
Jay Gopalakrishnan,
Joachim Schöberl,
Christoph Wintersteiger
Abstract:
Finite element methods for symmetric linear hyperbolic systems using unstructured advancing fronts (satisfying a causality condition) are considered in this work. Convergence results and error bounds are obtained for mapped tent pitching schemes made with standard discontinuous Galerkin discretizations for spatial approximation on mapped tents. Techniques to study semidiscretization on mapped tent…
▽ More
Finite element methods for symmetric linear hyperbolic systems using unstructured advancing fronts (satisfying a causality condition) are considered in this work. Convergence results and error bounds are obtained for mapped tent pitching schemes made with standard discontinuous Galerkin discretizations for spatial approximation on mapped tents. Techniques to study semidiscretization on mapped tents, design fully discrete schemes, prove local error bounds, prove stability on spacetime fronts, and bound error propagated through unstructured layers are developed.
△ Less
Submitted 14 July, 2021; v1 submitted 12 January, 2021;
originally announced January 2021.
-
Structure aware Runge-Kutta time step** for spacetime tents
Authors:
Jay Gopalakrishnan,
Joachim Schöberl,
Christoph Wintersteiger
Abstract:
We introduce a new class of Runge-Kutta type methods suitable for time step** to propagate hyperbolic solutions within tent-shaped spacetime regions. Unlike standard Runge-Kutta methods, the new methods yield expected convergence properties when standard high order spatial (discontinuous Galerkin) discretizations are used. After presenting a derivation of nonstandard order conditions for these m…
▽ More
We introduce a new class of Runge-Kutta type methods suitable for time step** to propagate hyperbolic solutions within tent-shaped spacetime regions. Unlike standard Runge-Kutta methods, the new methods yield expected convergence properties when standard high order spatial (discontinuous Galerkin) discretizations are used. After presenting a derivation of nonstandard order conditions for these methods, we show numerical examples of nonlinear hyperbolic systems to demonstrate the optimal convergence rates. We also report on the discrete stability properties of these methods applied to linear hyperbolic equations.
△ Less
Submitted 27 February, 2020;
originally announced February 2020.
-
Tent pitching and Trefftz-DG method for the acoustic wave equation
Authors:
Ilaria Perugia,
Joachim Schöberl,
Paul Stocker,
Christoph Wintersteiger
Abstract:
We present a space-time Trefftz discontinuous Galerkin method for approximating the acoustic wave equation semi-explicitly on tent pitched meshes. DG Trefftz methods use discontinuous test and trial functions, which solve the wave equation locally. Tent pitched meshes allow to solve the equation elementwise, allowing locally optimal advances in time. The method is implemented in NGSolve, solving t…
▽ More
We present a space-time Trefftz discontinuous Galerkin method for approximating the acoustic wave equation semi-explicitly on tent pitched meshes. DG Trefftz methods use discontinuous test and trial functions, which solve the wave equation locally. Tent pitched meshes allow to solve the equation elementwise, allowing locally optimal advances in time. The method is implemented in NGSolve, solving the space-time elements in parallel, whenever possible. Insights into the implementational details are given, including the case of propagation in heterogeneous media.
△ Less
Submitted 8 October, 2021; v1 submitted 4 July, 2019;
originally announced July 2019.
-
An Explicit Mapped Tent Pitching Scheme for Maxwell Equations
Authors:
Jay Gopalakrishnan,
Matthias Hochsteger,
Joachim Schöberl,
Christoph Wintersteiger
Abstract:
We present a new numerical method for solving time dependent Maxwell equations, which is also suitable for general linear hyperbolic equations. It is based on an unstructured partitioning of the spacetime domain into tent-shaped regions that respect causality. Provided that an approximate solution is available at the tent bottom, the equation can be locally evolved up to the top of the tent. By ma…
▽ More
We present a new numerical method for solving time dependent Maxwell equations, which is also suitable for general linear hyperbolic equations. It is based on an unstructured partitioning of the spacetime domain into tent-shaped regions that respect causality. Provided that an approximate solution is available at the tent bottom, the equation can be locally evolved up to the top of the tent. By map** tents to a domain which is a tensor product of a spatial domain with a time interval, it is possible to construct a fully explicit scheme that advances the solution through unstructured meshes. This work highlights a difficulty that arises when standard explicit Runge Kutta schemes are used in this context and proposes an alternative structure-aware Taylor time-step** technique. Thus explicit methods are constructed that allow variable time steps and local refinements without compromising high order accuracy in space and time. These Mapped Tent Pitching (MTP) schemes lead to highly parallel algorithms, which utilize modern computer architectures extremely well.
△ Less
Submitted 26 June, 2019;
originally announced June 2019.
-
Exploring Approximations for Floating-Point Arithmetic using UppSAT
Authors:
Aleksandar Zeljic,
Peter Backeman,
Christoph M. Wintersteiger,
Philipp Ruemmer
Abstract:
We consider the problem of solving floating-point constraints obtained from software verification. We present UppSAT --- a new implementation of a systematic approximation refinement framework [ZWR17] as an abstract SMT solver. Provided with an approximation and a decision procedure (implemented in an off-the-shelf SMT solver), UppSAT yields an approximating SMT solver. Additionally, UppSAT includ…
▽ More
We consider the problem of solving floating-point constraints obtained from software verification. We present UppSAT --- a new implementation of a systematic approximation refinement framework [ZWR17] as an abstract SMT solver. Provided with an approximation and a decision procedure (implemented in an off-the-shelf SMT solver), UppSAT yields an approximating SMT solver. Additionally, UppSAT includes a library of predefined approximation components which can be combined and extended to define new encodings, orderings and solving strategies. We propose that UppSAT can be used as a sandbox for easy and flexible exploration of new approximations. To substantiate this, we explore several approximations of floating-point arithmetic. Approximations can be viewed as a composition of an encoding into a target theory, a precision ordering, and a number of strategies for model reconstruction and precision (or approximation) refinement. We present encodings of floating-point arithmetic into reduced precision floating-point arithmetic, real-arithmetic, and fixed-point arithmetic (encoded in the theory of bit-vectors). In an experimental evaluation, we compare the advantages and disadvantages of approximating solvers obtained by combining various encodings and decision procedures (based on existing state-of-the-art SMT solvers for floating-point, real, and bit-vector arithmetic).
△ Less
Submitted 11 December, 2017; v1 submitted 23 November, 2017;
originally announced November 2017.
-
Relating Complexity-theoretic Parameters with SAT Solver Performance
Authors:
Edward Zulkoski,
Ruben Martins,
Christoph Wintersteiger,
Robert Robere,
Jia Liang,
Krzysztof Czarnecki,
Vijay Ganesh
Abstract:
Over the years complexity theorists have proposed many structural parameters to explain the surprising efficiency of conflict-driven clause-learning (CDCL) SAT solvers on a wide variety of large industrial Boolean instances. While some of these parameters have been studied empirically, until now there has not been a unified comparative study of their explanatory power on a comprehensive benchmark.…
▽ More
Over the years complexity theorists have proposed many structural parameters to explain the surprising efficiency of conflict-driven clause-learning (CDCL) SAT solvers on a wide variety of large industrial Boolean instances. While some of these parameters have been studied empirically, until now there has not been a unified comparative study of their explanatory power on a comprehensive benchmark. We correct this state of affairs by conducting a large-scale empirical evaluation of CDCL SAT solver performance on nearly 7000 industrial and crafted formulas against several structural parameters such as backdoors, treewidth, backbones, and community structure.
Our study led us to several results. First, we show that while such parameters only weakly correlate with CDCL solving time, certain combinations of them yield much better regression models. Second, we show how some parameters can be used as a "lens" to better understand the efficiency of different solving heuristics. Finally, we propose a new complexity-theoretic parameter, which we call learning-sensitive with restarts (LSR) backdoors, that extends the notion of learning-sensitive (LS) backdoors to incorporate restarts and discuss algorithms to compute them. We mathematically prove that for certain class of instances minimal LSR-backdoors are exponentially smaller than minimal-LS backdoors.
△ Less
Submitted 26 June, 2017;
originally announced June 2017.
-
Higher order unfitted FEM for Stokes interface problems
Authors:
Philip Lederer,
Carl-Martin Pfeiler,
Christoph Wintersteiger,
Christoph Lehrenfeld
Abstract:
We consider the discretization of a stationary Stokes interface problem in a velocity-pressure formulation. The interface is described implicitly as the zero level of a scalar function as it is common in level set based methods. Hence, the interface is not aligned with the mesh. An unfitted finite element discretization based on a Taylor-Hood velocity-pressure pair and an XFEM (or CutFEM) modifica…
▽ More
We consider the discretization of a stationary Stokes interface problem in a velocity-pressure formulation. The interface is described implicitly as the zero level of a scalar function as it is common in level set based methods. Hence, the interface is not aligned with the mesh. An unfitted finite element discretization based on a Taylor-Hood velocity-pressure pair and an XFEM (or CutFEM) modification is used for the approximation of the solution. This allows for the accurate approximation of solutions which have strong or weak discontinuities across interfaces which are not aligned with the mesh. To arrive at a consistent, stable and accurate formulation we require several additional techniques. First, a Nitsche-type formulation is used to implement interface conditions in a weak sense. Secondly, we use the ghost penalty stabilization to obtain an inf-sup stable variational formulation. Finally, for the highly accurate approximation of the implicitly described geometry, we use a combination of a piecewise linear interface reconstruction and a parametric map** of the underlying mesh. We introduce the method and discuss results of numerical examples.
△ Less
Submitted 13 May, 2016;
originally announced May 2016.
-
Mapped tent pitching schemes for hyperbolic systems
Authors:
J. Gopalakrishnan,
J. Schöberl,
C. Wintersteiger
Abstract:
A spacetime domain can be progressively meshed by tent shaped objects. Numerical methods for solving hyperbolic systems using such tent meshes to advance in time have been proposed previously. Such schemes have the ability to advance in time by different amounts at different spatial locations. This paper explores a technique by which standard discretizations, including explicit time step**, can…
▽ More
A spacetime domain can be progressively meshed by tent shaped objects. Numerical methods for solving hyperbolic systems using such tent meshes to advance in time have been proposed previously. Such schemes have the ability to advance in time by different amounts at different spatial locations. This paper explores a technique by which standard discretizations, including explicit time step**, can be used within tent-shaped spacetime domains. The technique transforms the equations within a spacetime tent to a domain where space and time are separable. After detailing techniques based on this map**, several examples including the acoustic wave equation and the Euler system are considered.
△ Less
Submitted 30 October, 2016; v1 submitted 4 April, 2016;
originally announced April 2016.
-
Lazy Decomposition for Distributed Decision Procedures
Authors:
Youssef Hamadi,
Joao Marques-Silva,
Christoph M. Wintersteiger
Abstract:
The increasing popularity of automated tools for software and hardware verification puts ever increasing demands on the underlying decision procedures. This paper presents a framework for distributed decision procedures (for first-order problems) based on Craig interpolation. Formulas are distributed in a lazy fashion, i.e., without the use of costly decomposition algorithms. Potential models whic…
▽ More
The increasing popularity of automated tools for software and hardware verification puts ever increasing demands on the underlying decision procedures. This paper presents a framework for distributed decision procedures (for first-order problems) based on Craig interpolation. Formulas are distributed in a lazy fashion, i.e., without the use of costly decomposition algorithms. Potential models which are shown to be incorrect are reconciled through the use of Craig interpolants. Experimental results on challenging propositional satisfiability problems indicate that our method is able to outperform traditional solving techniques even without the use of additional resources.
△ Less
Submitted 1 November, 2011;
originally announced November 2011.
