-
A Verified Information-Flow Architecture
Authors:
Arthur Azevedo de Amorim,
Nathan Collins,
André DeHon,
Delphine Demange,
Catalin Hritcu,
David Pichardie,
Benjamin C. Pierce,
Randy Pollack,
Andrew Tolmach
Abstract:
SAFE is a clean-slate design for a highly secure computer system, with pervasive mechanisms for tracking and limiting information flows. At the lowest level, the SAFE hardware supports fine-grained programmable tags, with efficient and flexible propagation and combination of tags as instructions are executed. The operating system virtualizes these generic facilities to present an information-flow…
▽ More
SAFE is a clean-slate design for a highly secure computer system, with pervasive mechanisms for tracking and limiting information flows. At the lowest level, the SAFE hardware supports fine-grained programmable tags, with efficient and flexible propagation and combination of tags as instructions are executed. The operating system virtualizes these generic facilities to present an information-flow abstract machine that allows user programs to label sensitive data with rich confidentiality policies. We present a formal, machine-checked model of the key hardware and software mechanisms used to dynamically control information flow in SAFE and an end-to-end proof of noninterference for this model.
We use a refinement proof methodology to propagate the noninterference property of the abstract machine down to the concrete machine level. We use an intermediate layer in the refinement chain that factors out the details of the information-flow control policy and devise a code generator for compiling such information-flow policies into low-level monitor code. Finally, we verify the correctness of this generator using a dedicated Hoare logic that abstracts from low-level machine instructions into a reusable set of verified structured code generators.
△ Less
Submitted 6 March, 2016; v1 submitted 22 September, 2015;
originally announced September 2015.
-
An asymptotically tight bound on the number of semi-algebraically connected components of realizable sign conditions
Authors:
Saugata Basu,
Richard Pollack,
Marie-Francoise Roy
Abstract:
We prove an asymptotically tight bound (asymptotic with respect to the number of polynomials for fixed degrees and number of variables) on the number of semi-algebraically connected components of the realizations of all realizable sign conditions of a family of real polynomials. More precisely, we prove that the number of semi-algebraically connected components of the realizations of all realiza…
▽ More
We prove an asymptotically tight bound (asymptotic with respect to the number of polynomials for fixed degrees and number of variables) on the number of semi-algebraically connected components of the realizations of all realizable sign conditions of a family of real polynomials. More precisely, we prove that the number of semi-algebraically connected components of the realizations of all realizable sign conditions of a family of $s$ polynomials in $\R[X_1,...,X_k]$ whose degrees are at most $d$ is bounded by \[ \frac{(2d)^k}{k!}s^k + O(s^{k-1}). \] This improves the best upper bound known previously which was \[ {1/2}\frac{(8d)^k}{k!}s^k + O(s^{k-1}). \] The new bound matches asymptotically the lower bound obtained for families of polynomials each of which is a product of generic polynomials of degree one.
△ Less
Submitted 14 July, 2009; v1 submitted 10 March, 2006;
originally announced March 2006.
-
Computing the First Betti Numberand Describing the Connected Components of Semi-algebraic Sets
Authors:
Saugata Basu,
Richard Pollack,
Marie-Francoise Roy
Abstract:
In this paper we describe a singly exponential algorithm for computing the first Betti number of a given semi-algebraic set. Singly exponential algorithms for computing the zero-th Betti number, and the Euler-Poincaré characteristic, were known before. No singly exponential algorithm was known for computing any of the individual Betti numbers other than the zero-th one. We also give algorithms f…
▽ More
In this paper we describe a singly exponential algorithm for computing the first Betti number of a given semi-algebraic set. Singly exponential algorithms for computing the zero-th Betti number, and the Euler-Poincaré characteristic, were known before. No singly exponential algorithm was known for computing any of the individual Betti numbers other than the zero-th one. We also give algorithms for obtaining semi-algebraic descriptions of the semi-algebraically connected components of any given real algebraic or semi-algebraic set in single-exponential time improving on previous results.
△ Less
Submitted 10 March, 2006;
originally announced March 2006.
