50 research outputs found
Tempus fugit: How to plug it
No full textSecret or private information may be leaked to an external attacker through the timing behaviour of the system running the untrusted code. After introducing a formalisation of this situation in terms of a confinement property, we present an algorithm which is able to transform the system into one that is computationally equivalent to the given system but free of timing leaks
Filling Out the Gaps: A Padding Algorithm for Transforming Out Timing Leaks
No full textAbstractIt has been shown that secret information can be leaked to external observers through covert timing channels. In this paper we are concerned with a kind of timing attack that wants to differentiate two processes, presented as probabilistic transition systems, by observing their timing behaviour. Our goal is to make the processes indistinguishable i.e. bisimilar, by adding virtual (dummy) states and transitions to the original processes (padding). Instead of padding the processes with whole virtual copies of their counterparts - as done by some padding algorithms - we present an algorithm that uses the bisimulation equivalence relation - computed as a lumping partition - as the main criterion to optimise the padding procedure
Constraint Systems for Useless Variable Elimination
No full textA useless variable is one whose value contributes nothing to the final outcome of a computation. Such variables are unlikely to occur in human-produced code, but may be introduced by various program transformations. We would like to eliminate useless parameters from procedures and eliminate the corresponding actual parameters from their call sites. This transformation is the extension to higherorder programming of a variety of dead-code elimination optimizations that are important in compilers for first-order imperative languages. Shivers has presented such a transformation. We reformulate the transformation and prove its correctness. We believe that this correctness proof can be a model for proofs of other analysis-based transformations. We proceed as follows: ffl We reformulate Shivers' analysis as a set of constraints; since the constraints are conditional inclusions, they can be solved using standard algorithms. ffl We prove that any solution to the constraints is sound: that tw..
Towards Verification of Well-Formed Transactions in Java Card Bytecode
No full textUsing transactions in Java Card bytecode programs can be rather tricky and requires special attention from the programmer in order to work around some of the limitations imposed and to avoid introducing serious run-time errors due to inappropriate use of transactions. In this paper we present a novel analysis that combines control and data flow analysis with an analysis that tracks active transactions in a Java Card bytecode program. We formally prove the correctness of the analysis and show how it can be used to solve the above problem of guaranteeing that transactions in a Java Card bytecode program are well-formed and thus do not give rise to run-time errors
Operational semantics of the Java Card Virtual Machine
No full textAbstractWe present the operational semantics of Carmel, a language that models the Java Card Virtual Machine Language. We define a small-step relation between program configurations, including rules for exception handling, array objects and subroutines. We also include the basic structures needed to model object ownership and the Java Card firewall
Bayesian phylodynamic inference with complex models
No full textPopulation genetic modeling can enhance Bayesian phylogenetic inference by providing a realistic prior on the distribution of branch lengths and times of common ancestry. The parameters of a population genetic model may also have intrinsic importance, and simultaneous estimation of a phylogeny and model parameters has enabled phylodynamic inference of population growth rates, reproduction numbers, and effective population size through time. Phylodynamic inference based on pathogen genetic sequence data has emerged as useful supplement to epidemic surveillance, however commonly-used mechanistic models that are typically fitted to non-genetic surveillance data are rarely fitted to pathogen genetic data due to a dearth of software tools, and the theory required to conduct such inference has been developed only recently. We present a framework for coalescent-based phylogenetic and phylodynamic inference which enables highly-flexible modeling of demographic and epidemiological processes. This approach builds upon previous structured coalescent approaches and includes enhancements for computational speed, accuracy, and stability. A flexible markup language is described for translating parametric demographic or epidemiological models into a structured coalescent model enabling simultaneous estimation of demographic or epidemiological parameters and time-scaled phylogenies. We demonstrate the utility of these approaches by fitting compartmental epidemiological models to Ebola virus and Influenza A virus sequence data, demonstrating how important features of these epidemics, such as the reproduction number and epidemic curves, can be gleaned from genetic data. These approaches are provided as an open-source package PhyDyn for the BEAST2 phylogenetics platform
Exploiting Sparsity in Polyhedral Analysis: 12th International Symposium, SAS 2005, London, UK, September 7-9, 2005. Proceedings
No full textThe intrinsic cost of polyhedra has lead to research on more tractable sub-classes of linear inequalities. Rather than committing to the precision of such a sub-class, this paper presents a projection algorithm that works directly on any sparse system of inequalities and which sacrifices precision only when necessary. The algorithm is based on a novel combination of the Fourier-Motzkin algorithm (for exact projection) and Simplex (for approximate projection). By reformulating the convex hull operation in terms of projection, conversion to the frame representation is avoided altogether. Experimental results conducted on logic programs demonstrate that the resulting analysis is efficient and precise
Bayesian phylodynamic inference with complex models
No full textAbstractPopulation genetic modeling can enhance Bayesian phylogenetic inference by providing a realistic prior on the distribution of branch lengths and times of common ancestry.The parameters of a population genetic model may also have intrinsic importance, and simultaneous estimation of a phylogeny and model parameters has enabled phylodynamic inference of population growth rates, reproduction numbers, and effective population size through time. Phylodynamic inference based on pathogen genetic sequence data has emerged as useful supplement to epidemic surveillance, however commonly-used mechanistic models that are typically fitted to non-genetic surveillance data are rarely fitted to pathogen genetic data due to a dearth of software tools, and the theory required to conduct such inference has been developed only recently. We present a framework for coalescent-based phylogenetic and phylodynamic inference which enables highly-flexible modeling of demographic and epidemiological processes. This approach builds upon previous structured coalescent approaches and includes enhancements for computational speed, accuracy, and stability. A flexible markup language is described for translating parametric demographic or epidemiological models into a structured coalescent model enabling simultaneous estimation of demographic or epidemiological parameters and time-scaled phylogenies. We demonstrate the utility of these approaches by fitting compartmental epidemiological models to Ebola virus and Influenza A virus sequence data, demonstrating how important features of these epidemics, such as the reproduction number and epidemic curves, can be gleaned from genetic data. These approaches are provided as an open-source packagePhyDynfor the BEAST phylogenetics platform.</jats:p
Constraint Systems for Useless Variable Elimination
No full textA useless variable is one whose value contributes nothing to the final outcome of a computation. Such variables are unlikely to occur in human-produced code, but may be introduced by various program transformations. We would like to eliminate useless parameters from procedures and eliminate the corresponding actual parameters from their call sites. This transformation is the extension to higher-order programming of a variety of dead-code elimination optimizations that are important in compilers for first-order imperative languages. Shivers has presented such a transformation. We reformulate the transformation and prove its correctness. We believe that this correctness proof can be a model for proofs of other analysis-based transformations. We proceed as follows: ffl We reformulate Shivers' analysis as a set of constraints; since the constraints are conditional inclusions, they can be solved using standard algorithms. ffl We prove that any solution to the constraints is sound: that tw..
Model-based estimates of cumulative infections through time for the 2014-15 Ebola epidemic in Western Africa.
No full textEstimates are shown for the SEIR model (A) and the model which includes super-spreading (B). The red line show the cumulative number of cases reported by WHO [35].</p
