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. ^

Community college adjunct policies and practices: Incumbents' perspectives and congruence with learning organization tenets

The primary research question was: What is the nature and degree of alignment between the tenets of learning organizations and the policies and practices of a community college concerning adjunct instructors? I investigated the employment experiences of 8 adjunct instructors at a large community college in the Southeastern U.S. to (a) describe and explain the perspectives of the adjuncts, (b) describe and explain my own adjunct employment experience at the same college, (c) determine how the adjunct policies and practices collectively encountered were congruent with or at variance with the tenets of learning organizations, and (d) to use this framework to support recommendations that may help the college achieve more favorable alignment with these tenets. ^ Data on perceived adjunct policies and practices were reduced into 11 categories and, using matrices, were compared with 5 major categories of learning organization tenets. The 5 categories of tenets were: (a) inputs, (b) information flow/communication, (c) employee inclusion/value, (d) teamwork, and (e) facilitation of change. The 11 categories of the college's policies and practices were (a) becoming an adjunct, (b) full-time employment aspirations, (c) salary, (d) benefits, (e) job security and predictability, (f) job satisfaction, (g) respect, (h) support services, (i) professional development, (j) institutional inclusion, and (k) future role of adjuncts. The reflective journal component relied on a 5-year (1995–2000) personal and professional journal maintained by me during employment with the same college as the participants. ^ Findings indicate that the college's adjunct policies and practices were most incongruent with 25 of the 70 learning organization tenets. These incongruencies spanned the 5 categories, although most occurred in the Employee/Inclusion/Value category. Adjunct instructors wanted inclusion, respect, value, trust, and empowerment in decision making processes that affect adjunct policies and practices of the college, but did not perceive this to be a part of the present situation. ^

A software tool that generates symbolic model verifier (SMV) input language from a predicate transition net

The purpose of this research was to apply model checking by using a symbolic model checker on Predicate Transition Nets (PrT Nets). A PrT Net is a formal model of information flow which allows system properties to be modeled and analyzed. The aim of this thesis was to use the modeling and analysis power of PrT nets to provide a mechanism for the system model to be verified. Symbolic Model Verifier (SMV) was the model checker chosen in this thesis, and in order to verify the PrT net model of a system, it was translated to SMV input language. A software tool was implemented which translates the PrT Net into SMV language, hence enabling the process of model checking. The system includes two parts: the PrT net editor where the representation of a system can be edited, and the translator which converts the PrT net into an SMV program.

Information Discovery on Electronic Health Records Using Authority Flow Techniques

Background As the use of electronic health records (EHRs) becomes more widespread, so does the need to search and provide effective information discovery within them. Querying by keyword has emerged as one of the most effective paradigms for searching. Most work in this area is based on traditional Information Retrieval (IR) techniques, where each document is compared individually against the query. We compare the effectiveness of two fundamentally different techniques for keyword search of EHRs. Methods We built two ranking systems. The traditional BM25 system exploits the EHRs' content without regard to association among entities within. The Clinical ObjectRank (CO) system exploits the entities' associations in EHRs using an authority-flow algorithm to discover the most relevant entities. BM25 and CO were deployed on an EHR dataset of the cardiovascular division of Miami Children's Hospital. Using sequences of keywords as queries, sensitivity and specificity were measured by two physicians for a set of 11 queries related to congenital cardiac disease. Results Our pilot evaluation showed that CO outperforms BM25 in terms of sensitivity (65% vs. 38%) by 71% on average, while maintaining the specificity (64% vs. 61%). The evaluation was done by two physicians. Conclusions Authority-flow techniques can greatly improve the detection of relevant information in EHRs and hence deserve further study.

A comparative study of life history and gene flow in darters (Pisces: Percidae)

Gene flow, or the exchange of genes between populations, is important because it determines the evolutionary trajectory of a species, including the relative influences of genetic drift and natural selection in the process of population differentiation. Gene flow differs among species because of variation in dispersal capability and abundances across taxa, and historical forces related to geological or lineage history. Both history and ecology influence gene flow in potentially complicated ways, and accounting for their effects remains an important problem in evolutionary biology. This research is a comparative study of gene flow and life-history in a monophyletic group of stream fishes, the darters. As a first step in disentangling historical and ecological effects, I reconstructed the phylogenetic relationships of the study species from nucleotide sequences in the mtDNA control region. I then used this phylogeny and regional glaciation history to infer historical effects on life-history evolution and gene flow in 15 species of darters. Gene flow was estimated indirectly, using information from 20 resolvable and polymorphic allozyme loci. When I accounted for historical effects, comparisons across taxa revealed that gene flow rates were closely associated with differences in clutch sizes and reproductive investment patterns. I hypothesized that differences in larval dispersal among taxa explained this relationship. Results from a field study of larval drift were consistent with this hypothesis. Finally, I asked whether there was an interaction between species' ecology and genetic differentiation across biogeographically distinct regions. Information from allozymes and mtDNA sequences revealed that life history plays an important role in the magnitude of species divergence across biogeographic boundaries. These results suggested an important association between life histories and rates of speciation following an allopatric isolation event. This research, along with other studies from the literature, further illustrates the enormous potential of North American freshwater fishes as a system for studying speciation processes. ^

The impact of information technology on organizations: A study of enterprise resource planning system influences on job design and organizational culture

The primary purpose of this research is to study the linkage between perceived job design characteristics and information system environment characteristics before and after the replacement of a legacy information system with a new type of information system (referred to as an Enterprise Resource Planning or ERP system). A public state University implementing an academic version of an ERP system was selected for the study. Three survey instruments were used to examine the perception of the information system, the job characteristics, and the organizational culture before and after the system implementation. The research participants included two large departments resulting in a sample of 130 workers. Research questions were analyzed using multivariate procedures including factor analysis, path analysis, step-wise regression, and matched pair analysis. ^ Results indicated that the ERP system has introduced new elements into the working environment that has changed the perception of how the job design characteristics and organization culture dimensions are viewed by the workers. The understanding of how the perceived system characteristics align with an individual's perceived job design characteristics is supported by each of the system characteristics significantly correlated in the proposed direction. The stronger support of this relationship becomes visible in the causal flow of the effects seen in the path diagram and in the step-wise regression. The perceived job design characteristics aligning with dimensions of organizational culture are not as strong as the literature suggests. Although there are significant correlations between the job and culture variables, only one relationship can be seen in the causal flow. ^ This research has demonstrated that system characteristics of ERP do contribute to the perception of change in an organization and do support organizational culture behaviors and job characteristics. ^

Multidimensional classification and diagnosis of leukemia in flow cytometry

This research is to establish new optimization methods for pattern recognition and classification of different white blood cells in actual patient data to enhance the process of diagnosis. Beckman-Coulter Corporation supplied flow cytometry data of numerous patients that are used as training sets to exploit the different physiological characteristics of the different samples provided. The methods of Support Vector Machines (SVM) and Artificial Neural Networks (ANN) were used as promising pattern classification techniques to identify different white blood cell samples and provide information to medical doctors in the form of diagnostic references for the specific disease states, leukemia. The obtained results prove that when a neural network classifier is well configured and trained with cross-validation, it can perform better than support vector classifiers alone for this type of data. Furthermore, a new unsupervised learning algorithm---Density based Adaptive Window Clustering algorithm (DAWC) was designed to process large volumes of data for finding location of high data cluster in real-time. It reduces the computational load to ∼O(N) number of computations, and thus making the algorithm more attractive and faster than current hierarchical algorithms.

Surface mean flow and turbulence structure in tropical cyclone winds

Hurricanes are one of the deadliest and costliest natural hazards affecting the Gulf coast and Atlantic coast areas of the United States. An effective way to minimize hurricane damage is to strengthen structures and buildings. The investigation of surface level hurricane wind behavior and the resultant wind loads on structures is aimed at providing structural engineers with information on hurricane wind characteristics required for the design of safe structures. Information on mean wind profiles, gust factors, turbulence intensity, integral scale, and turbulence spectra and co-spectra is essential for developing realistic models of wind pressure and wind loads on structures. The research performed for this study was motivated by the fact that considerably fewer data and validated models are available for tropical than for extratropical storms. ^ Using the surface wind measurements collected by the Florida Coastal Monitoring Program (FCMP) during hurricane passages over coastal areas, this study presents comparisons of surface roughness length estimates obtained by using several estimation methods, and estimates of the mean wind and turbulence structure of hurricane winds over coastal areas under neutral stratification conditions. In addition, a program has been developed and tested to systematically analyze Wall of Wind (WoW) data, that will make it possible to perform analyses of baseline characteristics of flow obtained in the WoW. This program can be used in future research to compare WoW data with FCMP data, as gust and turbulence generator systems and other flow management devices will be used to create WoW flows that match as closely as possible real hurricane wind conditions. ^ Hurricanes are defined as tropical cyclones for which the maximum 1-minute sustained surface wind speeds exceed 74 mph. FCMP data include data for tropical cyclones with lower sustained speeds. However, for the winds analyzed in this study the speeds were sufficiently high to assure that neutral stratification prevailed. This assures that the characteristics of those winds are similar to those prevailing in hurricanes. For this reason in this study the terms tropical cyclones and hurricanes are used interchangeably. ^

Drosophila Flight Stabilization Depends on Apparent Distances in Optic Flow Field

To perform daily flight tasks, insects rely heavily on their visual perception of a dynamic environment. They must process visual signals quickly and accurately and update their behavior. Flies are vulnerable to environmental disturbances, such as gusts of wind blowing them off course, but they may use the altered visual field to compensate and regain their original course. In studies using Drosophila melanogaster, it has been shown that their corrective responses can be analyzed by measuring changes in their wing beats. By enclosing a tethered fly in a cuboidal visual arena displaying a computerized optic flow field, it is possible to calculate the change in wing beat amplitudes from an infrared shadow of its wings using photodiodes and a custom wing beat analyzer. In this experiment, manipulations ofthe optic flow field are used to create a field where points have varying relative forward speed, to study how the insect performs corrective maneuvers. The results show that Drosophila have a stronger corrective response to the quickly moving, apparently near points compared to the slower moving, apparently distant points. This implies the flies are distinguishing points based on their relative speeds, inferring distance, and adjusting their corrective actions with this information.

Surface Mean Flow and Turbulence Structure in Tropical Cyclone Winds

Hurricanes are one of the deadliest and costliest natural hazards affecting the Gulf coast and Atlantic coast areas of the United States. An effective way to minimize hurricane damage is to strengthen structures and buildings. The investigation of surface level hurricane wind behavior and the resultant wind loads on structures is aimed at providing structural engineers with information on hurricane wind characteristics required for the design of safe structures. Information on mean wind profiles, gust factors, turbulence intensity, integral scale, and turbulence spectra and co-spectra is essential for developing realistic models of wind pressure and wind loads on structures. The research performed for this study was motivated by the fact that considerably fewer data and validated models are available for tropical than for extratropical storms. Using the surface wind measurements collected by the Florida Coastal Monitoring Program (FCMP) during hurricane passages over coastal areas, this study presents comparisons of surface roughness length estimates obtained by using several estimation methods, and estimates of the mean wind and turbulence structure of hurricane winds over coastal areas under neutral stratification conditions. In addition, a program has been developed and tested to systematically analyze Wall of Wind (WoW) data, that will make it possible to perform analyses of baseline characteristics of flow obtained in the WoW. This program can be used in future research to compare WoW data with FCMP data, as gust and turbulence generator systems and other flow management devices will be used to create WoW flows that match as closely as possible real hurricane wind conditions. Hurricanes are defined as tropical cyclones for which the maximum 1-minute sustained surface wind speeds exceed 74 mph. FCMP data include data for tropical cyclones with lower sustained speeds. However, for the winds analyzed in this study the speeds were sufficiently high to assure that neutral stratification prevailed. This assures that the characteristics of those winds are similar to those prevailing in hurricanes. For this reason in this study the terms tropical cyclones and hurricanes are used interchangeably.

Numerical groundwater flow modeling in the Wakal River basin, India

Increasing dependence on groundwater in the Wakal River basin, India, jeopardizes water supply sustainability. A numerical groundwater model was developed to better understand the aquifer system and to evaluate its potential in terms of quantity and replenishment. Potential artificial recharge areas were delineated using landscape and hydrogeologic parameters, Geographic Information System (GIS), and remote sensing. Groundwater models are powerful tools for recharge estimation when transmissivity is known. Proper recharge must be applied to reproduce field-measured heads. The model showed that groundwater levels could decline significantly if there are two drought years in every four years that result in reduced recharge, and groundwater withdrawal is increased by 15%. The effect of such drought is currently uncertain however, because runoff from the basin is unknown. Remote sensing and GIS revealed areas with slopes less than 5%, forest cover, and Normalized Difference Vegetative Index greater than 0.5 that are suitable recharge sites.

Design and Development of Geographical Information System (GIS) Map for Nuclear Waste Streams

A nuclear waste stream is the complete flow of waste material from origin to treatment facility to final disposal. The objective of this study was to design and develop a Geographic Information Systems (GIS) module using Google Application Programming Interface (API) for better visualization of nuclear waste streams that will identify and display various nuclear waste stream parameters. A proper display of parameters would enable managers at Department of Energy waste sites to visualize information for proper planning of waste transport. The study also developed an algorithm using quadratic Bézier curve to make the map more understandable and usable. Microsoft Visual Studio 2012 and Microsoft SQL Server 2012 were used for the implementation of the project. The study has shown that the combination of several technologies can successfully provide dynamic mapping functionality. Future work should explore various Google Maps API functionalities to further enhance the visualization of nuclear waste streams.