-
Reconciling Shannon and Scott with a Lattice of Computable Information
Authors:
Sebastian Hunt,
David Sands,
Sandro Stucki
Abstract:
This paper proposes a reconciliation of two different theories of information. The first, originally proposed in a lesser-known work by Claude Shannon, describes how the information content of channels can be described qualitatively, but still abstractly, in terms of information elements, i.e. equivalence relations over the data source domain. Shannon showed that these elements form a complete lat…
▽ More
This paper proposes a reconciliation of two different theories of information. The first, originally proposed in a lesser-known work by Claude Shannon, describes how the information content of channels can be described qualitatively, but still abstractly, in terms of information elements, i.e. equivalence relations over the data source domain. Shannon showed that these elements form a complete lattice, with the order expressing when one element is more informative than another. In the context of security and information flow this structure has been independently rediscovered several times, and used as a foundation for reasoning about information flow.
The second theory of information is Dana Scott's domain theory, a mathematical framework for giving meaning to programs as continuous functions over a particular topology. Scott's partial ordering also represents when one element is more informative than another, but in the sense of computational progress, i.e. when one element is a more defined or evolved version of another.
To give a satisfactory account of information flow in programs it is necessary to consider both theories together, to understand what information is conveyed by a program viewed as a channel (à la Shannon) but also by the definedness of its encoding (à la Scott). We combine these theories by defining the Lattice of Computable Information (LoCI), a lattice of preorders rather than equivalence relations. LoCI retains the rich lattice structure of Shannon's theory, filters out elements that do not make computational sense, and refines the remaining information elements to reflect how Scott's ordering captures the way that information is presented.
We show how the new theory facilitates the first general definition of termination-insensitive information flow properties, a weakened form of information flow property commonly targeted by static program analyses.
△ Less
Submitted 3 February, 2023; v1 submitted 18 November, 2022;
originally announced November 2022.
-
Monitoring Data Minimisation
Authors:
Srinivas Pinisetty,
Thibaud Antignac,
David Sands,
Gerardo Schneider
Abstract:
Data minimisation is a privacy enhancing principle, stating that personal data collected should be no more than necessary for the specific purpose consented by the user. Checking that a program satisfies the data minimisation principle is not easy, even for the simple case when considering deterministic programs-as-functions. In this paper we prove (im)possibility results concerning runtime monito…
▽ More
Data minimisation is a privacy enhancing principle, stating that personal data collected should be no more than necessary for the specific purpose consented by the user. Checking that a program satisfies the data minimisation principle is not easy, even for the simple case when considering deterministic programs-as-functions. In this paper we prove (im)possibility results concerning runtime monitoring of (non-)minimality for deterministic programs both when the program has one input source (monolithic) and for the more general case when inputs come from independent sources (distributed case). We propose monitoring mechanisms where a monitor observes the inputs and the outputs of a program, to detect violation of data minimisation policies. We show that monitorability of (non) minimality is decidable only for specific cases, and detection of satisfaction of different notions of minimality in undecidable in general. That said, we show that under certain conditions monitorability is decidable and we provide an algorithm and a bound to check such properties in a pre-deployment controlled environment, also being able to compute a minimiser for the given program. Finally, we provide a proof-of-concept implementation for both offline and online monitoring and apply that to some case studies.
△ Less
Submitted 5 January, 2018;
originally announced January 2018.
-
Data Minimisation: a Language-Based Approach (Long Version)
Authors:
Thibaud Antignac,
David Sands,
Gerardo Schneider
Abstract:
Data minimisation is a privacy-enhancing principle considered as one of the pillars of personal data regulations. This principle dictates that personal data collected should be no more than necessary for the specific purpose consented by the user. In this paper we study data minimisation from a programming language perspective. We assume that a given program embodies the purpose of data collection…
▽ More
Data minimisation is a privacy-enhancing principle considered as one of the pillars of personal data regulations. This principle dictates that personal data collected should be no more than necessary for the specific purpose consented by the user. In this paper we study data minimisation from a programming language perspective. We assume that a given program embodies the purpose of data collection, and define a data minimiser as a pre-processor for the input which reduces the amount of information available to the program without compromising its functionality. In this context we study formal definitions of data minimisation, present different mechanisms and architectures to ensure data minimisation, and provide a procedure to synthesise a correct data minimiser for a given program.
△ Less
Submitted 17 November, 2016;
originally announced November 2016.
-
Featherweight PINQ
Authors:
Hamid Ebadi,
David Sands
Abstract:
Differentially private mechanisms enjoy a variety of composition properties. Leveraging these, McSherry introduced PINQ (SIGMOD 2009), a system empowering non-experts to construct new differentially private analyses. PINQ is an LINQ-like API which provides automatic privacy guarantees for all programs which use it to mediate sensitive data manipulation. In this work we introduce featherweight PINQ…
▽ More
Differentially private mechanisms enjoy a variety of composition properties. Leveraging these, McSherry introduced PINQ (SIGMOD 2009), a system empowering non-experts to construct new differentially private analyses. PINQ is an LINQ-like API which provides automatic privacy guarantees for all programs which use it to mediate sensitive data manipulation. In this work we introduce featherweight PINQ, a formal model capturing the essence of PINQ. We prove that any program interacting with featherweight PINQ's API is differentially private.
△ Less
Submitted 11 May, 2015;
originally announced May 2015.
-
The Anatomy and Facets of Dynamic Policies
Authors:
Niklas Broberg,
Bart van Delft,
David Sands
Abstract:
Information flow policies are often dynamic; the security concerns of a program will typically change during execution to reflect security-relevant events. A key challenge is how to best specify, and give proper meaning to, such dynamic policies. A large number of approaches exist that tackle that challenge, each yielding some important, but unconnected, insight. In this work we synthesise existin…
▽ More
Information flow policies are often dynamic; the security concerns of a program will typically change during execution to reflect security-relevant events. A key challenge is how to best specify, and give proper meaning to, such dynamic policies. A large number of approaches exist that tackle that challenge, each yielding some important, but unconnected, insight. In this work we synthesise existing knowledge on dynamic policies, with an aim to establish a common terminology, best practices, and frameworks for reasoning about them. We introduce the concept of facets to illuminate subtleties in the semantics of policies, and closely examine the anatomy of policies and the expressiveness of policy specification mechanisms. We further explore the relation between dynamic policies and the concept of declassification.
△ Less
Submitted 23 September, 2015; v1 submitted 8 May, 2015;
originally announced May 2015.
-
Very Static Enforcement of Dynamic Policies
Authors:
Bart van Delft,
Sebastian Hunt,
David Sands
Abstract:
Security policies are naturally dynamic. Reflecting this, there has been a growing interest in studying information-flow properties which change during program execution, including concepts such as declassification, revocation, and role-change.
A static verification of a dynamic information flow policy, from a semantic perspective, should only need to concern itself with two things: 1) the depen…
▽ More
Security policies are naturally dynamic. Reflecting this, there has been a growing interest in studying information-flow properties which change during program execution, including concepts such as declassification, revocation, and role-change.
A static verification of a dynamic information flow policy, from a semantic perspective, should only need to concern itself with two things: 1) the dependencies between data in a program, and 2) whether those dependencies are consistent with the intended flow policies as they change over time. In this paper we provide a formal ground for this intuition. We present a straightforward extension to the principal flow-sensitive type system introduced by Hunt and Sands (POPL '06, ESOP '11) to infer both end-to-end dependencies and dependencies at intermediate points in a program. This allows ty**s to be applied to verification of both static and dynamic policies. Our extension preserves the principal type system's distinguishing feature, that type inference is independent of the policy to be enforced: a single, generic dependency analysis (ty**) can be used to verify many different dynamic policies of a given program, thus achieving a clean separation between (1) and (2).
We also make contributions to the foundations of dynamic information flow. Arguably, the most compelling semantic definitions for dynamic security conditions in the literature are phrased in the so-called knowledge-based style. We contribute a new definition of knowledge-based termination insensitive security for dynamic policies. We show that the new definition avoids anomalies of previous definitions and enjoys a simple and useful characterisation as a two-run style property.
△ Less
Submitted 12 January, 2015;
originally announced January 2015.
-
Type-Directed Compilation for Fault-Tolerant Non-Interference
Authors:
Filippo Del Tedesco,
David Sands,
Alejandro Russo
Abstract:
Environmental noise (e.g.heat, ionized particles, etc.) causes transient faults in hardware, which lead to corruption of stored values. Mission-critical devices require such faults to be mitigated by fault-tolerance --- a combination of techniques that aim at preserving the functional behaviour of a system despite the disruptive effects of transient faults. Fault-tolerance typically has a high dep…
▽ More
Environmental noise (e.g.heat, ionized particles, etc.) causes transient faults in hardware, which lead to corruption of stored values. Mission-critical devices require such faults to be mitigated by fault-tolerance --- a combination of techniques that aim at preserving the functional behaviour of a system despite the disruptive effects of transient faults. Fault-tolerance typically has a high deployment cost -- special hardware might be required to implement it -- and provides weak statistical guarantees. It is also based on the assumption that faults are rare. In this paper, we consider scenarios where security, rather than functional correctness, is the main asset to be protected. Our contribution is twofold. Firstly, we develop a theory for expressing confidentiality of data in the presence of transient faults. We show that the natural probabilistic definition of security in the presence of faults can be captured by a possibilistic definition. Furthermore, the possibilistic definition is implied by a known bisimulation-based property, called Strong Security. Secondly, we illustrate the utility of these results for a simple RISC architecture for which only the code memory and program counter are assumed fault-tolerant. We present a type-directed compilation scheme that produces RISC code from a higher-level language for which Strong Security holds --- i.e. well-typed programs compile to RISC code which is secure despite transient faults. In contrast with fault-tolerance solutions, our technique assumes relatively little special hardware, gives formal guarantees, and works in the presence of an active attacker who aggressively targets parts of a system and induces faults precisely.
△ Less
Submitted 25 October, 2014; v1 submitted 18 October, 2014;
originally announced October 2014.
-
Reinterpreting Boltzmann's H-theorem in the light of Information Theory
Authors:
David Sands,
Jeremy Dunning-Davies
Abstract:
Prompted by the realisation that the statistical entropy of an ideal gas in the micro-canonical ensemble should not fluctuate or change over time, the meaning of the H-theorem is re-interpreted from the perspective of information theory in which entropy is a measure of uncertainty. We propose that the Maxwellian velocity distribution should more properly be regarded as a limiting distribution whic…
▽ More
Prompted by the realisation that the statistical entropy of an ideal gas in the micro-canonical ensemble should not fluctuate or change over time, the meaning of the H-theorem is re-interpreted from the perspective of information theory in which entropy is a measure of uncertainty. We propose that the Maxwellian velocity distribution should more properly be regarded as a limiting distribution which is identical with the distribution across particles in the asymptotic limit of large numbers. In smaller systems, the distribution across particles differs from the limiting distribution and fluctuates. Therefore the entropy can be calculated either from the actual distribution across the particles or from the limiting distribution. The former fluctuates with the distribution but the latter does not. However, only the latter represents uncertainty in the sense implied by information theory by accounting for all possible microstates. We also argue that the Maxwellian probability distribution for the velocity of a single particle should be regarded as a limiting distribution. Therefore the entropy of a single particle is well defined, as is the entropy of an N-particle system, regardless of the microstate. We argue that the meaning of the H-theorem is to reveal the underlying distribution in the limit of large numbers. Computer simulations of a hard-sphere fluid are used to demonstrate the ideas.
△ Less
Submitted 7 January, 2013;
originally announced January 2013.
-
Gender differences in conceptual understanding of Newtonian mechanics: a UK cross-institution comparison
Authors:
Simon Bates,
Robyn Donnelly,
Cait MacPhee,
David Sands,
Marion Birch,
Niels R. Walet
Abstract:
We present results of a combined study from three UK universities where we investigate the existence and persistence of a performance gender gap in conceptual understanding of Newtonian mechanics. Using the Force Concept Inventory, we find that students at all three universities exhibit a statistically significant gender gap, with males outperforming females. This gap is narrowed but not eliminate…
▽ More
We present results of a combined study from three UK universities where we investigate the existence and persistence of a performance gender gap in conceptual understanding of Newtonian mechanics. Using the Force Concept Inventory, we find that students at all three universities exhibit a statistically significant gender gap, with males outperforming females. This gap is narrowed but not eliminated after instruction, using a variety of instructional approaches. Furthermore, we find that before instruction the quartile with the lowest performance on the diagnostic instrument comprises a disproportionately high fraction (~50%) of the total female cohort. The majority of these students remain in the lowest-performing quartile post-instruction. Analysis of responses to individual items shows that male students outperform female students on practically all items on the instrument. Comparing the performance of the same group of students on end-of-course examinations, we find no statistically significant gender gaps.
△ Less
Submitted 16 November, 2012;
originally announced November 2012.
-
A Semantic Hierarchy for Erasure Policies
Authors:
Filippo Del Tedesco,
Sebastian Hunt,
David Sands
Abstract:
We consider the problem of logical data erasure, contrasting with physical erasure in the same way that end-to-end information flow control contrasts with access control. We present a semantic hierarchy for erasure policies, using a possibilistic knowledge-based semantics to define policy satisfaction such that there is an intuitively clear upper bound on what information an erasure policy permits…
▽ More
We consider the problem of logical data erasure, contrasting with physical erasure in the same way that end-to-end information flow control contrasts with access control. We present a semantic hierarchy for erasure policies, using a possibilistic knowledge-based semantics to define policy satisfaction such that there is an intuitively clear upper bound on what information an erasure policy permits to be retained. Our hierarchy allows a rich class of erasure policies to be expressed, taking account of the power of the attacker, how much information may be retained, and under what conditions it may be retained. While our main aim is to specify erasure policies, the semantic framework allows quite general information-flow policies to be formulated for a variety of semantic notions of secrecy.
△ Less
Submitted 30 September, 2011;
originally announced September 2011.
-
Room Temperature Device Performance of Electrodeposited InSb Nanowire Field Effect Transistors
Authors:
Suprem R. Das,
Collin J. Delker,
Dmitri Zakharov,
Yong P. Chen,
Timothy D. Sands,
David B. Janes
Abstract:
In this study, InSb nanowires have been formed by electrodeposition and integrated into NW-FETs. NWs were formed in porous anodic alumina (PAA) templates, with the PAA pore diameter of approximately 100 nm defining the NW diameter. Following annealing at 125C and 420C respectively, the nanowires exhibited the zinc blende crystalline structure of InSb, as confirmed from x-ray diffraction and high r…
▽ More
In this study, InSb nanowires have been formed by electrodeposition and integrated into NW-FETs. NWs were formed in porous anodic alumina (PAA) templates, with the PAA pore diameter of approximately 100 nm defining the NW diameter. Following annealing at 125C and 420C respectively, the nanowires exhibited the zinc blende crystalline structure of InSb, as confirmed from x-ray diffraction and high resolution transmission electron microscopy. The annealed nanowires were used to fabricate nanowire field effect transistors (NW-FET) each containing a single NW with 500 nm channel length and gating through a 20nm SiO2 layer on a doped Si wafer. Following annealing of the NW-FETs at 300C for 10 minutes in argon ambient, transistor characteristics were observed with an ION ~ 40 uA (at VDS = 1V in a back-gate configuration), ION/IOFF ~ 16 - 20 in the linear regime of transistor operation and gd ~ 71uS. The field effect electron mobility extracted from the transconductance was ~1200 cm2 V-1 s-1 at room temperature. We report high on-current per nanowire compared with other reported NW-FETs with back-gate geometry and current saturation at low source-drain voltages. The device characteristics are not well described by long-channel MOSFET models, but can qualitatively be understood in terms of velocity saturation effects accounting for enhanced scattering
△ Less
Submitted 28 April, 2011;
originally announced April 2011.
-
Confusion in Thermodynamics
Authors:
Jeremy Dunning-Davies,
David Sands
Abstract:
For a long time now, confusion has existed in the minds of many over the meaning of various concepts in thermodynamics. Recently, this point has been brought to people's attention by two articles appearing on the well-known archive (arxiv) web site. The content of these two pieces serves to illustrate many of the problems and has occasioned the construction of this answer to at least some of them.…
▽ More
For a long time now, confusion has existed in the minds of many over the meaning of various concepts in thermodynamics. Recently, this point has been brought to people's attention by two articles appearing on the well-known archive (arxiv) web site. The content of these two pieces serves to illustrate many of the problems and has occasioned the construction of this answer to at least some of them. The position of the axiom proposed by Carathéodory is central in this matter and here its position is clarified and secured within the framework of thermodynamics. In particular, its relation to the First Law is examined and justified.
△ Less
Submitted 17 May, 2011; v1 submitted 2 March, 2011;
originally announced March 2011.
-
Titanium nitride as a plasmonic material for visible wavelengths
Authors:
Gururaj V. Naik,
Jeremy L. Schroeder,
Timothy D. Sands,
Alexandra Boltasseva
Abstract:
The search for alternative plasmonic materials with improved optical properties over the traditional materials like silver and gold could ultimately lead to the long-awaited, real-life applications of plasmonic devices and metamaterials. In this work, we show that titanium nitride could perform as an alternative plasmonic material in the visible wavelength range. We evaluate the performances of va…
▽ More
The search for alternative plasmonic materials with improved optical properties over the traditional materials like silver and gold could ultimately lead to the long-awaited, real-life applications of plasmonic devices and metamaterials. In this work, we show that titanium nitride could perform as an alternative plasmonic material in the visible wavelength range. We evaluate the performances of various plasmonic and metamaterial structures with titanium nitride as a plasmonic component and show that transformation-optics devices and an important class of metamaterials with hyperbolic dispersion based on TiN could significantly outperform similar devices based on conventional metals in the visible wavelengths range.
△ Less
Submitted 26 November, 2010; v1 submitted 22 November, 2010;
originally announced November 2010.
-
Specification and Verification of Side Channel Declassification
Authors:
Josef Svenningsson,
David Sands
Abstract:
Side channel attacks have emerged as a serious threat to the security of both networked and embedded systems -- in particular through the implementations of cryptographic operations. Side channels can be difficult to model formally, but with careful coding and program transformation techniques it may be possible to verify security in the presence of specific side-channel attacks. But what if a p…
▽ More
Side channel attacks have emerged as a serious threat to the security of both networked and embedded systems -- in particular through the implementations of cryptographic operations. Side channels can be difficult to model formally, but with careful coding and program transformation techniques it may be possible to verify security in the presence of specific side-channel attacks. But what if a program intentionally makes a tradeoff between security and efficiency and leaks some information through a side channel? In this paper we study such tradeoffs using ideas from recent research on declassification. We present a semantic model of security for programs which allow for declassification through side channels, and show how side-channel declassification can be verified using off-the-shelf software model checking tools. Finally, to make it simpler for verifiers to check that a program conforms to a particular side-channel declassification policy we introduce a further tradeoff between efficiency and verifiability: by writing programs in a particular "manifest form" security becomes considerably easier to verify.
△ Less
Submitted 15 December, 2009;
originally announced December 2009.
-
A User Model for Information Erasure
Authors:
Filippo Del Tedesco,
David Sands
Abstract:
Hunt and Sands (ESOP'08) studied a notion of information erasure for systems which receive secrets intended for limited-time use. Erasure demands that once a secret has fulfilled its purpose the subsequent behaviour of the system should reveal no information about the erased data. In this paper we address a shortcoming in that work: for erasure to be possible the user who provides data must also…
▽ More
Hunt and Sands (ESOP'08) studied a notion of information erasure for systems which receive secrets intended for limited-time use. Erasure demands that once a secret has fulfilled its purpose the subsequent behaviour of the system should reveal no information about the erased data. In this paper we address a shortcoming in that work: for erasure to be possible the user who provides data must also play his part, but previously that role was only specified informally. Here we provide a formal model of the user and a collection of requirements called erasure friendliness. We prove that an erasure-friendly user can be composed with an erasing system (in the sense of Hunt and Sands) to obtain a combined system which is jointly erasing in an appropriate sense. In doing so we identify stronger requirements on the user than those informally described in the previous work.
△ Less
Submitted 21 October, 2009;
originally announced October 2009.
-
Higher order Schwarzian derivatives in interval dynamics
Authors:
O. Kozlovski,
D. Sands
Abstract:
We introduce an infinite sequence of higher order Schwarzian derivatives closely related to the theory of monotone matrix functions. We generalize the classical Koebe lemma to maps with positive Schwarzian derivatives up to some order, obtaining control over derivatives of high order. For a large class of multimodal interval maps we show that all inverse branches of first return maps to sufficie…
▽ More
We introduce an infinite sequence of higher order Schwarzian derivatives closely related to the theory of monotone matrix functions. We generalize the classical Koebe lemma to maps with positive Schwarzian derivatives up to some order, obtaining control over derivatives of high order. For a large class of multimodal interval maps we show that all inverse branches of first return maps to sufficiently small neighbourhoods of critical values have their higher order Schwarzian derivatives positive up to any given order.
△ Less
Submitted 14 December, 2008;
originally announced December 2008.
-
Thermodynamic Entropy And The Accessible States of Some Simple Systems
Authors:
David Sands
Abstract:
Comparison of the thermodynamic entropy with Boltzmann's principle shows that under conditions of constant volume the total number of arrangements in simple thermodynamic systems with temperature-independent heat capacities is TC/k. A physical interpretation of this function is given for three such systems; an ideal monatomic gas, an ideal gas of diatomic molecules with rotational motion, and a…
▽ More
Comparison of the thermodynamic entropy with Boltzmann's principle shows that under conditions of constant volume the total number of arrangements in simple thermodynamic systems with temperature-independent heat capacities is TC/k. A physical interpretation of this function is given for three such systems; an ideal monatomic gas, an ideal gas of diatomic molecules with rotational motion, and a solid in the Dulong-Petit limit of high temperature. T1/2 emerges as a natural measure of the number of accessible states for a single particle in one dimension. Extension to N particles in three dimensions leads to TC/k as the total number of possible arrangements or microstates. The different microstates of the system are thus shown a posteriori to be equally probable, with probability T-C/k, which implies that for the purposes of counting states the particles of the gas are distinguishable. The most probable energy state of the system is determined by the degeneracy of the microstates.
△ Less
Submitted 12 August, 2007;
originally announced August 2007.
-
The Canonical Ensemble and the Central Limit Theorem
Authors:
D. Sands,
J. Dunning-Davies
Abstract:
Some of the more powerful results of mathematical statistics are becoming of increasing importance in statistical mechanics. Here the use of the central limit theorem in conjunction with the canonical ensemble is shown to lead to an interesting and important new insight into results associated with the canonical ensemble. This theoretical work is illustrated numerically and it is shown how this…
▽ More
Some of the more powerful results of mathematical statistics are becoming of increasing importance in statistical mechanics. Here the use of the central limit theorem in conjunction with the canonical ensemble is shown to lead to an interesting and important new insight into results associated with the canonical ensemble. This theoretical work is illustrated numerically and it is shown how this numerical work can form the basis of an undergraduate laboratory experiment which should help to implant ideas of statistical mechanics in students' minds.
△ Less
Submitted 7 June, 2007;
originally announced June 2007.
-
Metric attractors for smooth unimodal maps
Authors:
Jacek Graczyk,
Duncan Sands,
Grzegorz Swiatek
Abstract:
We classify the measure theoretic attractors of general C^3 unimodal maps with quadratic critical points. The main ingredient is the decay of geometry.
We classify the measure theoretic attractors of general C^3 unimodal maps with quadratic critical points. The main ingredient is the decay of geometry.
△ Less
Submitted 6 January, 2006;
originally announced January 2006.
