Noninterference is a technique to formally capture the intuitive notion of information flow in the context of security. Information does not flow from one agent to another if the actions of the first have no impact on the future observations of the second. Various formulations of this notion have been proposed based on state machines and the removal of actions from action sequences. A new model known as the concurrent game structure [CGS] has recently been introduced for analysis multi-agent systems. We propose an alternate formulation of noninterference defined for systems modeled by CGS's and analyze the impact of the new approach on noninterference research based on existing definitions.

Information flow security concerns how to protect sensitive data in computer systems by avoiding undesirable flow of information between the users of the systems. This thesis studies information flow security properties in state-based systems, dealing in particular with modelling and verification methods for asynchronous systems and synchronous systems with schedulers. The aim of this study is to provide a foundational guide to ensure confidentiality in system design and verification. The thesis begins with a study of definitions of security properties in asynchronous models. Two classes of security notions are of particular interest. Trace-based properties disallow deductions of high security level secrets from low level observation traces. Bisimulation-based properties express security as a low-level observational equivalence relation on states. In the literature, several distinct schools have developed frameworks for information flow security properties based on different semantic domains. One of the major contributions of the thesis is a systematic study that compares security notions, using semantic mappings between two state-based models and a particular process algebraic model. An advantage of state-based models is the availability of well-developed verification methods and tools for functional properties in finite state systems. The thesis investigates the application of these methods to the algorithmic verification of the information flow security properties in the asynchronous settings. The complexity bounds for verifying these security properties are given as polynomial time for the bisimulation-based properties and polynomial space complete for the trace-based properties. Two heuristics are presented to benefit the verifications of the properties in practice. Timing channels are one of the major concerns in the computer security community, but are not captured in asynchronous models. In the final part of the thesis, a new system model is defined that deals with timing and scheduling. A group of novel security notions, including both trace-based and bisimulation-based properties, are proposed in this new model. It is further investigated whether these security properties are preserved by refinement of schedulers and scheduler implementations. A case study of a multi- evel secure file server is described, which applies a number of access control rules to enforce a particular bisimulation-based property in the synchronous setting.

Information flow security concerns how to protect sensitive data in computer systems by avoiding undesirable flow of information between the users of the systems. This thesis studies information flow security properties in state-based systems, dealing in particular with modelling and verification methods for asynchronous systems and synchronous systems with schedulers. The aim of this study is to provide a foundational guide to ensure confidentiality in system design and verification. The thesis begins with a study of definitions of security properties in asynchronous models. Two classes of security notions are of particular interest. Trace-based properties disallow deductions of high security level secrets from low level observation traces. Bisimulation-based properties express security as a low-level observational equivalence relation on states. In the literature, several distinct schools have developed frameworks for information flow security properties based on different semantic domains. One of the major contributions of the thesis is a systematic study that compares security notions, using semantic mappings between two state-based models and a particular process algebraic model. An advantage of state-based models is the availability of well-developed verification methods and tools for functional properties in finite state systems. The thesis investigates the application of these methods to the algorithmic verification of the information flow security properties in the asynchronous settings. The complexity bounds for verifying these security properties are given as polynomial time for the bisimulation-based properties and polynomial space complete for the trace-based properties. Two heuristics are presented to benefit the verifications of the properties in practice. Timing channels are one of the major concerns in the computer security community, but are not captured in asynchronous models. In the final part of the thesis, a new system model is defined that deals with timing and scheduling. A group of novel security notions, including both trace-based and bisimulation-based properties, are proposed in this new model. It is further investigated whether these security properties are preserved by refinement of schedulers and scheduler implementations. A case study of a multi- evel secure file server is described, which applies a number of access control rules to enforce a particular bisimulation-based property in the synchronous setting.

Ingeniero Civil en Computación / La protección de la confidencialidad de la información manipulada por los programas computacionales es abordada a nivel del código fuente con distintas técnicas. Una de ellas es tipado de seguridad para el control de flujo, que controla el nivel de seguridad donde fluye la información agregando anotaciones a las variables tipadas. La propiedad de seguridad fundamental de control de flujo es conocida como no-interferencia (noninterference), que establece que un observador público no puede obtener conocimiento desde datos confidenciales. A pesar de ser una propiedad muy atractiva, los sistemas reales la vulneran fácilmente, y necesitan mecanismos para desclasificar selectivamente alguna información. En esta dirección, Cruz et al. proponen una forma de desclasificación basada en tipos (type-based declassification), en donde se utilizan las relaciones de subtipos del lenguaje para expresar las políticas de desclasificación de los datos que maneja el programa, en una forma simple y expresiva. A pesar de que el fundamento teórico de la desclasificación basada en tipos está bien descrito, carece de una implementación que permita comprobar la utilidad práctica de la propuesta. En este trabajo, se implementa el análisis de la desclasificación basada en tipos para un subconjunto del lenguaje Dart, un lenguaje de programación de propósito general orientado a objetos desarrollado por Google. Además, se implementó un sistema de inferencia de políticas de desclasificación y una extensión para ambientes de desarrollo, con el objetivo de facilitar el trabajo al programador y mejorar su experiencia.

The recent years have seen the revival of neo-Roman republicanism through the works of Philip Pettit, who has replaced Isaiah Berlin’s taxonomy of positive/negative liberty with freedom as nondomination. This essay compares the neo-Roman conception of nondomination to the liberal conception of noninterference, with the purpose of clarifying whether nondomination is a distinct concept of liberty and preferable to that of noninterference. The essay highlights the exchange between Pettit/Skinner and Carter/Kramer, wherein Carter and Kramer make their case for ‘pure negative liberty’, which is claimed to be the proper articulation of negative liberty. Pure-negative theorists believe that nondomination is a strand of negative liberty, adding nothing new to the concept, whereas their republican counterparts disagree. My essay argues that nondomination is a distinct, preferable concept of liberty, thanks to its view on fundamental unfreedom and the mere presence of arbitrary power, which the pure negative view fails to account for satisfactorily.