Verifying abstract information flow properties in fault tolerant security devices

The verification of information flow properties of security devices is difficult because it involves the analysis of schematic diagrams, artwork, embedded software, etc. In addition, a typical security device has many modes, partial information flow, and needs to be fault tolerant. We propose a new approach to the verification of such devices based upon checking abstract information flow properties expressed as graphs. This approach has been implemented in software, and successfully used to find possible paths of information flow through security devices.

Practical secure information flow in programming languages

If we classify variables in a program into various security levels, then a secure information flow analysis aims to verify statically that information in a program can flow only in ways consistent with the specified security levels. One well-studied approach is to formulate the rules of the secure information flow analysis as a type system. A major trend of recent research focuses on how to accommodate various sophisticated modern language features. However, this approach often leads to overly complicated and restrictive type systems, making them unfit for practical use. Also, problems essential to practical use, such as type inference and error reporting, have received little attention. This dissertation identified and solved major theoretical and practical hurdles to the application of secure information flow. ^ We adopted a minimalist approach to designing our language to ensure a simple lenient type system. We started out with a small simple imperative language and only added features that we deemed most important for practical use. One language feature we addressed is arrays. Due to the various leaking channels associated with array operations, arrays have received complicated and restrictive typing rules in other secure languages. We presented a novel approach for lenient array operations, which lead to simple and lenient typing of arrays. ^ Type inference is necessary because usually a user is only concerned with the security types for input/output variables of a program and would like to have all types for auxiliary variables inferred automatically. We presented a type inference algorithm B and proved its soundness and completeness. Moreover, algorithm B stays close to the program and the type system and therefore facilitates informative error reporting that is generated in a cascading fashion. Algorithm B and error reporting have been implemented and tested. ^ Lastly, we presented a novel framework for developing applications that ensure user information privacy. In this framework, core computations are defined as code modules that involve input/output data from multiple parties. Incrementally, secure flow policies are refined based on feedback from the type checking/inference. Core computations only interact with code modules from involved parties through well-defined interfaces. All code modules are digitally signed to ensure their authenticity and integrity. ^

Secure information flow via stripping and fast simulation

Type systems for secure information flow aim to prevent a program from leaking information from H (high) to L (low) variables. Traditionally, bisimulation has been the prevalent technique for proving the soundness of such systems. This work introduces a new proof technique based on stripping and fast simulation, and shows that it can be applied in a number of cases where bisimulation fails. We present a progressive development of this technique over a representative sample of languages including a simple imperative language (core theory), a multiprocessing nondeterministic language, a probabilistic language, and a language with cryptographic primitives. In the core theory we illustrate the key concepts of this technique in a basic setting. A fast low simulation in the context of transition systems is a binary relation where simulating states can match the moves of simulated states while maintaining the equivalence of low variables; stripping is a function that removes high commands from programs. We show that we can prove secure information flow by arguing that the stripping relation is a fast low simulation. We then extend the core theory to an abstract distributed language under a nondeterministic scheduler. Next, we extend to a probabilistic language with a random assignment command; we generalize fast simulation to the setting of discrete time Markov Chains, and prove approximate probabilistic noninterference. Finally, we introduce cryptographic primitives into the probabilistic language and prove computational noninterference, provided that the underling encryption scheme is secure.

Foundations of quantitative information flow: Channels, cascades, and the information order

Secrecy is fundamental to computer security, but real systems often cannot avoid leaking some secret information. For this reason, the past decade has seen growing interest in quantitative theories of information flow that allow us to quantify the information being leaked. Within these theories, the system is modeled as an information-theoretic channel that specifies the probability of each output, given each input. Given a prior distribution on those inputs, entropy-like measures quantify the amount of information leakage caused by the channel. ^ This thesis presents new results in the theory of min-entropy leakage. First, we study the perspective of secrecy as a resource that is gradually consumed by a system. We explore this intuition through various models of min-entropy consumption. Next, we consider several composition operators that allow smaller systems to be combined into larger systems, and explore the extent to which the leakage of a combined system is constrained by the leakage of its constituents. Most significantly, we prove upper bounds on the leakage of a cascade of two channels, where the output of the first channel is used as input to the second. In addition, we show how to decompose a channel into a cascade of channels. ^ We also establish fundamental new results about the recently-proposed g-leakage family of measures. These results further highlight the significance of channel cascading. We prove that whenever channel A is composition refined by channel B, that is, whenever A is the cascade of B and R for some channel R, the leakage of A never exceeds that of B, regardless of the prior distribution or leakage measure (Shannon leakage, guessing entropy leakage, min-entropy leakage, or g-leakage). Moreover, we show that composition refinement is a partial order if we quotient away channel structure that is redundant with respect to leakage alone. These results are strengthened by the proof that composition refinement is the only way for one channel to never leak more than another with respect to g-leakage. Therefore, composition refinement robustly answers the question of when a channel is always at least as secure as another from a leakage point of view.^

Two-bit pattern analysis for quantitative information flow

Protecting confidential information from improper disclosure is a fundamental security goal. While encryption and access control are important tools for ensuring confidentiality, they cannot prevent an authorized system from leaking confidential information to its publicly observable outputs, whether inadvertently or maliciously. Hence, secure information flow aims to provide end-to-end control of information flow. Unfortunately, the traditionally-adopted policy of noninterference, which forbids all improper leakage, is often too restrictive. Theories of quantitative information flow address this issue by quantifying the amount of confidential information leaked by a system, with the goal of showing that it is intuitively "small" enough to be tolerated. Given such a theory, it is crucial to develop automated techniques for calculating the leakage in a system. ^ This dissertation is concerned with program analysis for calculating the maximum leakage, or capacity, of confidential information in the context of deterministic systems and under three proposed entropy measures of information leakage: Shannon entropy leakage, min-entropy leakage, and g-leakage. In this context, it turns out that calculating the maximum leakage of a program reduces to counting the number of possible outputs that it can produce. ^ The new approach introduced in this dissertation is to determine two-bit patterns, the relationships among pairs of bits in the output; for instance we might determine that two bits must be unequal. By counting the number of solutions to the two-bit patterns, we obtain an upper bound on the number of possible outputs. Hence, the maximum leakage can be bounded. We first describe a straightforward computation of the two-bit patterns using an automated prover. We then show a more efficient implementation that uses an implication graph to represent the two- bit patterns. It efficiently constructs the graph through the use of an automated prover, random executions, STP counterexamples, and deductive closure. The effectiveness of our techniques, both in terms of efficiency and accuracy, is shown through a number of case studies found in recent literature. ^

Tiedonkulun merkitys erilaisissa tuotannonohjausympäristöissä

Tämä kandidaatintyö käsittelee yrityksen sisäisen tiedonkulun merkitystä erilaisissa tuotannonohjausympäristöissä. Työn tavoitteena on selvittää millaisia tietotarpeita tuotannonohjauksella on, miten tuotannonohjausmuoto vaikuttaa tietotarpeisiin sekä onko puutteellisen tiedonkulun seurauksilla erilainen merkitys asiakastilauksen kytkentäpisteen (CODP) mukaisissa tuotantoympäristöissä. Lisäksi työ antaa teoriakatsauksen tuotannonohjausprosessista sekä yrityksen sisäisestä tiedonkulusta. Tutkielman perusteella voidaan todeta, että tuotannonohjausmuodot vaikuttavat tietotarpeisiin ja että puutteellisen tiedonkulun seurauksilla on erilainen merkitys erilaisissa tuotantoympäristöissä. Yleisesti voidaan todeta, että mitä aikaisemmassa vaiheessa CODP on, sitä merkittävämpiä seuraukset ovat. Koska sisäisen tiedonkulun, tuotannonohjausmuotojen sekä puutteellisen tiedonkulun seurausten välisestä merkityksestä ei ole varsinaisesti julkaistu aiempaa tutkimusta, olisi lisätutkimus myös tarpeellista.

Information and Material Flows in Project Business

Tavoitteena diplomityössä oli kuvata projektiliiketoimintaa harjoittavan yrityksen informaatio- ja materiaalivirrat toimitusprojekteissa. Selvitys haluttiin tehdä tulevia kehitysprojekteja varten. Diplomityö toteutettiin kahessa osassa: laatimalla aiheeseen liittyvä teoriakatsaus ja kartoittamalla todellinen tilanne yrityksen sisällä.Teoriaosassa kuvattiin tarkastelualue ja projektiliiketoiminnan erityispiirteitä sekä käsiteltiin tietojärjestelmiä ja materiaalivirran hallintaan liittyviä asioita. Yrityksen informaatio- ja materiaalivirtojen nykytila kartoitettiin laatimalla vuokaaviot kolmen esimerkkituotteen toimitusprojekteista. Kaaviot laadittiin yrityksen sisäisten dokumenttien ja kvalitatiivisten haastattelujen pohjalta. Kaavioiden sisältöä täydennettiin taulukoimalla kaavioissa esiintyvien dokumettien sisältöä. Työn tuloksena muodostui kuva tiedonkäsittelyn nykytilasta myynti- ja toimitusprojekteissa, pelkistetty visio tulevaisuuden tietojärjestelmien rooleista sekä ehdotuksia tulevia kehitysprojekteja varten.

Information management in aircraft maintenance

Well managed information promotes competitive advantage and economic value for the company. The challenge is to use information effectively in complex networks. Decision making in network is complicated due to many independent sources of information. The aim of the present study was to identify and map the internal information flows and used information resourced by functions and roles, to make proposals to the case organization to improve the information management and to improve the situational awareness and process flows. In the present study, an inductive approach was applied, with the aim to find out gaps and bottlenecks of information flow of an aircraft maintenance organization and its network. The empirical part was conducted with observing the processes and with questionnaires. Theoretical part of this study consists on reviewing relevant literature on maintenance management in aviation and information management in aviation. Together with empirical evidence and the literature used in the study the gaps were found and suggestions for improvements were done. The outcome of this study contributes the organization in its bigger goal to improve the productivity. The information management of the network is one actor in the field and will pave the way to smoother operation and situational awareness. The lack of rules and requirements for information management and spreading is a challenge in information management. The excessive data overburden may cause problem in the actors’ situation-awareness due to non-availability of the right information.

Non-Markovianity through flow of information between a system and an environment

Conselho Nacional de Desenvolvimento Científico e Tecnológico (CNPq)

Development of a novel material flow simulation model for the integration of spatial and process relevant information

Simulation techniques are almost indispensable in the analysis of complex systems. Materials- and related information flow processes in logistics often possess such complexity. Further problem arise as the processes change over time and pose a Big Data problem as well. To cope with these issues adaptive simulations are more and more frequently used. This paper presents a few relevant advanced simulation models and intro-duces a novel model structure, which unifies modelling of geometrical relations and time processes. This way the process structure and their geometric relations can be handled in a well understandable and transparent way. Capabilities and applicability of the model is also presented via a demonstrational example.

THE INTERACTION BETWEEN INTERNAL AND EXTERNAL INFORMATION ON RELATIONAL DATA SEARCH

People often use tools to search for information. In order to improve the quality of an information search, it is important to understand how internal information, which is stored in user’s mind, and external information, represented by the interface of tools interact with each other. How information is distributed between internal and external representations significantly affects information search performance. However, few studies have examined the relationship between types of interface and types of search task in the context of information search. For a distributed information search task, how data are distributed, represented, and formatted significantly affects the user search performance in terms of response time and accuracy. Guided by UFuRT (User, Function, Representation, Task), a human-centered process, I propose a search model, task taxonomy. The model defines its relationship with other existing information models. The taxonomy clarifies the legitimate operations for each type of search task of relation data. Based on the model and taxonomy, I have also developed prototypes of interface for the search tasks of relational data. These prototypes were used for experiments. The experiments described in this study are of a within-subject design with a sample of 24 participants recruited from the graduate schools located in the Texas Medical Center. Participants performed one-dimensional nominal search tasks over nominal, ordinal, and ratio displays, and searched one-dimensional nominal, ordinal, interval, and ratio tasks over table and graph displays. Participants also performed the same task and display combination for twodimensional searches. Distributed cognition theory has been adopted as a theoretical framework for analyzing and predicting the search performance of relational data. It has been shown that the representation dimensions and data scales, as well as the search task types, are main factors in determining search efficiency and effectiveness. In particular, the more external representations used, the better search task performance, and the results suggest the ideal search performance occurs when the question type and corresponding data scale representation match. The implications of the study lie in contributing to the effective design of search interface for relational data, especially laboratory results, which are often used in healthcare activities.

Analysis of air flow past and through the 2415-3S airfoil for an unmanned aerial vehicle with internal propulsion system

This paper deals with the prediction of velocity fields on the 2415-3S airfoil which will be used for an unmanned aerial vehicle with internal propulsion system and in this way analyze the air flow through an internal duct of the airfoil using computational fluid dynamics. The main objective is to evaluate the effect of the internal air flow past the airfoil and how this affects the aerodynamic performance by means of lift and drag forces. For this purpose, three different designs of the internal duct were studied; starting from the base 2415-3S airfoil developed in previous investigation, basing on the hypothesis of decreasing the flow separation produced when the propulsive airflow merges the external flow, and in this way obtaining the best configuration. For that purpose, an exhaustive study of the mesh sensitivity was performed. It was used a non-structured mesh since the computational domain is three-dimensional and complex. The selected mesh contains approximately 12.5 million elements. Both the computational domain and the numerical solution were made with commercial CAD and CFD software, respectively. Air, incompressible and steady was analyzed. The boundary conditions are in concordance with experimental setup in the AF 6109 wind tunnel. The k-e model is utilized to describe the turbulent flow process as followed in references. Results allowed obtaining velocity contours as well as lift and drag coefficients and also the location of separation and reattachment regions in some cases for zero degrees of angle of attack on the internal and external surfaces of the airfoil. Finally, the selection of the configuration with the best aerodynamic performance was made, selecting the option without curved baffles.

Numerical analysis of air flow past the 2415-3S airfoil for an unmanned aerial vehicle with internal propulsion system

This paper deals with the prediction of pressure and velocity fields on the 2415-3S airfoil which will be used for and unmanned aerial vehicle with internal propulsion system and in this way analyze the air flow through an internal duct of the airfoil using computational fluid dynamics. The main objective is to evaluate the effect of the internal air flow past the airfoil and how this affects the aerodynamic performance by means of lift and drag forces. For this purpose, three different designs of the internal duct were studied; starting from the base 2415-3S airfoil developed in previous investigation, basing on the hypothesis of decreasing the flow separation produced when the propulsive airflow merges the external flow, and in this way obtaining the best configuration. For that purpose, an exhaustive study of the mesh sensitivity was performed. It was used a non-structured mesh since the computational domain is tridimensional and complex. The selected mesh contains approximately 12.5 million elements. Both the computational domain and the numerical solution were made with commercial CAD and CFD software respectively. Air, incompressible and steady was analyzed. The boundary conditions are in concordance with experimental setup in the AF 6109 wind tunnel. The k-ε model is utilized to describe the turbulent flow process as followed in references. Results allowed obtaining pressure and velocity contours as well as lift and drag coefficients and also the location of separation and reattachment regions in some cases for zero degrees of angle of attack on the internal and external surfaces of the airfoil. Finally, the selection of the configuration with the best aerodynamic performance was made, selecting the option without curved baffles.

AN ASSESSMENT OF FLOW REGIME MAPS AND A NUMERICAL HEAT TRANSFER CORRELATION FOR THE STRATIFIED/ANNULAR REGIME OF SHEAR-DRIVEN INTERNAL CONDENSING FLOWS

Several modern-day cooling applications require the incorporation of mini/micro-channel shear-driven flow condensers. There are several design challenges that need to be overcome in order to meet those requirements. The difficulty in developing effective design tools for shear-driven flow condensers is exacerbated due to the lack of a bridge between the physics-based modelling of condensing flows and the current, popular approach based on semi-empirical heat transfer correlations. One of the primary contributors of this disconnect is a lack of understanding caused by the fact that typical heat transfer correlations eliminate the dependence of the heat transfer coefficient on the method of cooling employed on the condenser surface when it may very well not be the case. This is in direct contrast to direct physics-based modeling approaches where the thermal boundary conditions have a direct and huge impact on the heat transfer coefficient values. Typical heat transfer correlations instead introduce vapor quality as one of the variables on which the value of the heat transfer coefficient depends. This study shows how, under certain conditions, a heat transfer correlation from direct physics-based modeling can be equivalent to typical engineering heat transfer correlations without making the same apriori assumptions. Another huge factor that raises doubts on the validity of the heat-transfer correlations is the opacity associated with the application of flow regime maps for internal condensing flows. It is well known that flow regimes influence heat transfer rates strongly. However, several heat transfer correlations ignore flow regimes entirely and present a single heat transfer correlation for all flow regimes. This is believed to be inaccurate since one would expect significant differences in the heat transfer correlations for different flow regimes. Several other studies present a heat transfer correlation for a particular flow regime - however, they ignore the method by which extents of the flow regime is established. This thesis provides a definitive answer (in the context of stratified/annular flows) to: (i) whether a heat transfer correlation can always be independent of the thermal boundary condition and represented as a function of vapor quality, and (ii) whether a heat transfer correlation can be independently obtained for a flow regime without knowing the flow regime boundary (even if the flow regime boundary is represented through a separate and independent correlation). To obtain the results required to arrive at an answer to these questions, this study uses two numerical simulation tools - the approximate but highly efficient Quasi-1D simulation tool and the exact but more expensive 2D Steady Simulation tool. Using these tools and the approximate values of flow regime transitions, a deeper understanding of the current state of knowledge in flow regime maps and heat transfer correlations in shear-driven internal condensing flows is obtained. The ideas presented here can be extended for other flow regimes of shear-driven flows as well. Analogous correlations can also be obtained for internal condensers in the gravity-driven and mixed-driven configuration.