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

Genetic individualization of Cannabis sativa by a short tandem repeat multiplex system

Cannabis sativa is the most frequently used of all illicit drugs in the United States. Cannabis has been used throughout history for its stems in the production of hemp fiber, for its seed for oil and food, and for its buds and leaves as a psychoactive drug. Short tandem repeats (STRs), were chosen as molecular markers because of their distinct advantages over other genetic methods. STRs are co-dominant, can be standardized such that reproducibility between laboratories can be easily achieved, have a high discrimination power and can be multiplexed. ^ In this study, six STR markers previously described for Cannabis were multiplexed into one reaction. The multiplex reaction was able to individualize 98 Cannabis samples (14 hemp and 84 marijuana, authenticated as originating from 33 of the 50 United States) and detect 29 alleles averaging 4.8 alleles per loci. The data did not relate the samples from the same state to each other. This is the first study to report a single reaction six-plex and apply it to the analysis of almost 100 Cannabis samples of known geographic collection site. ^