Type System for the ComponentJ Programming Language

Dissertação apresentada na Faculdade de Ciências e Tecnologia da Universidade Nova de Lisboa para a obtenção do grau de Mestre em Engenharia Informática.

A type system for access control in an object-oriented language

Trabalho apresentado no âmbito do Mestrado em Engenharia Informática, como requisito parcial para obtenção do grau de Mestre em Engenharia Informática

A type system for value-dependent information flow analysis

Information systems are widespread and used by anyone with computing devices as well as corporations and governments. It is often the case that security leaks are introduced during the development of an application. Reasons for these security bugs are multiple but among them one can easily identify that it is very hard to define and enforce relevant security policies in modern software. This is because modern applications often rely on container sharing and multi-tenancy where, for instance, data can be stored in the same physical space but is logically mapped into different security compartments or data structures. In turn, these security compartments, to which data is classified into in security policies, can also be dynamic and depend on runtime data. In this thesis we introduce and develop the novel notion of dependent information flow types, and focus on the problem of ensuring data confidentiality in data-centric software. Dependent information flow types fit within the standard framework of dependent type theory, but, unlike usual dependent types, crucially allow the security level of a type, rather than just the structural data type itself, to depend on runtime values. Our dependent function and dependent sum information flow types provide a direct, natural and elegant way to express and enforce fine grained security policies on programs. Namely programs that manipulate structured data types in which the security level of a structure field may depend on values dynamically stored in other fields The main contribution of this work is an efficient analysis that allows programmers to verify, during the development phase, whether programs have information leaks, that is, it verifies whether programs protect the confidentiality of the information they manipulate. As such, we also implemented a prototype typechecker that can be found at http://ctp.di.fct.unl.pt/DIFTprototype/.

BOUSSINESQ-TYPE SYSTEM OF EQUATIONS IN THE BENARD-MARANGONI SYSTEM

A system of coupled evolution equations for the bulk velocity and the surface displacement is found to govern the long-wavelength perturbations in a Benard-Marangoni system. This system of equations, involving nonlinearity, dispersion, and dissipation, is a generalization of the usual Boussinesq system.

A type system with usage aspects

Linear typing schemes can be used to guarantee non-interference and so the soundness of in-place update with respect to a functional semantics. But linear schemes are restrictive in practice, and more restrictive than necessary to guarantee soundness of in-place update. This limitation has prompted research into static analysis and more sophisticated typing disciplines to determine when in-place update may be safely used, or to combine linear and non-linear schemes. Here we contribute to this direction by defining a new typing scheme that better approximates the semantic property of soundness of in-place update for a functional semantics. We begin from the observation that some data are used only in a read-only context, after which it may be safely re-used before being destroyed. Formalising the in-place update interpretation in a machine model semantics allows us to refine this observation, motivating three usage aspects apparent from the semantics that are used to annotate function argument types. The aspects are (1) used destructively, (2), used read-only but shared with result, and (3) used read-only and not shared with the result. The main novelty is aspect (2), which allows a linear value to be safely read and even aliased with a result of a function without being consumed. This novelty makes our type system more expressive than previous systems for functional languages in the literature. The system remains simple and intuitive, but it enjoys a strong soundness property whose proof is non-trivial. Moreover, our analysis features principal types and feasible type reconstruction, as shown in M. Konen'y (In TYPES 2002 workshop, Nijmegen, Proceedings, Springer-Verlag, 2003).

Application of a PERT-Type System and "Crashing" in a Food Service Operation

A pert-type system, a combination of the program evaluation and review technique (PERT) and the critical path method (CPM), might be used by the hospitality industry to improve planning and control of complex functions. The author discusses this management science technique and how it can assist.

Transcriptional coupling between the divergent promoters of a prototypic LysR-type regulatory system, the ilvYC operon of Escherichia coli

The twin-domain model [Liu, L. F. & Wang, J. C. (1987) Proc. Natl. Acad. Sci. USA 84, 7024–7027] suggests that closely spaced, divergent, superhelically sensitive promoters can affect the transcriptional activity of one another by transcriptionally induced negative DNA supercoiling generated in the divergent promoter region. This gene arrangement is observed for many LysR-type-regulated operons in bacteria. We have examined the effects of divergent transcription in the prototypic LysR-type system, the ilvYC operon of Escherichia coli. Double-reporter constructs with the lacZ gene under transcriptional control of the ilvC promoter and the galK gene under control of the divergent ilvY promoter were used to demonstrate that a down-promoter mutation in the ilvY promoter severely decreases in vivo transcription from the ilvC promoter. However, a down-promoter mutation in the ilvC promoter only slightly affects transcription from the ilvY promoter. In vitro transcription assays with DNA topoisomers showed that transcription from the ilvC promoter increases over the entire range of physiological superhelical densities, whereas transcription initiation from the ilvY promoter exhibits a broad optimum at a midphysiological superhelical density. Evidence that this promoter coupling is DNA supercoiling-dependent is provided by the observation that a novobiocin-induced decrease in global negative superhelicity results in an increase in ilvY promoter activity and a decrease in ilvC promoter activity predicted by the in vitro data. We suggest that this transcriptional coupling is important for coordinating basal level expression of the ilvYC operon with the nutritional and environmental conditions of cell growth.

Type checking cryptography implementations

Cryptographic software development is a challenging eld: high performance must be achieved, while ensuring correctness and com- pliance with low-level security policies. CAO is a domain speci c language designed to assist development of cryptographic software. An important feature of this language is the design of a novel type system introducing native types such as prede ned sized vectors, matrices and bit strings, residue classes modulo an integer, nite elds and nite eld extensions, allowing for extensive static validation of source code. We present the formalisation, validation and implementation of this type system

Design and implementation of a behaviorally typed programming system for web services

Dissertação apresentada na Faculdade de Ciências e Tecnologia da Universidade Nova de Lisboa para a obtenção do Grau de Mestre em Engenharia Informática.

Type-based protocol conformance and aliasing control in concurrent java programs

Dissertação para obtenção do Grau de Mestre em Engenharia Informática

Stability of periodic optical solitons for a nonlinear Schrodinger system

This paper is concerned with the existence and nonlinear stability of periodic travelling-wave solutions for a nonlinear Schrodinger-type system arising in nonlinear optics. We show the existence of smooth curves of periodic solutions depending on the dnoidal-type functions. We prove stability results by perturbations having the same minimal wavelength, and instability behaviour by perturbations of two or more times the minima period. We also establish global well posedness for our system by using Bourgain`s approach.

Non-Ohmic and dielectric properties of a Ca2Cu2Ti4O12 polycrystalline system

An investigation was made into the non-Ohmic and dielectric properties of a Ca2Cu2Ti4O12 perovskite-type system. Compared to the traditional CaCu3Ti4O12-based composition, the imbalance between the Ca and Cu atoms caused the formation of a polycrystalline system presenting similar to 33.3 mol % of CaCu3Ti4O12 (traditional composition) and similar to 66.7 mol % of CaTiO3. As for non-Ohmic properties, the effect of this Ca and Cu atom imbalance was that a nonlinear electric behavior of similar to 1500 was obtained. This high nonlinear electrical behavior emerged in detriment to the ultrahigh dielectric property frequently reported. The high non-Ohmic property was explained by the existence of Schottky-type barriers, whose formation mechanism may be similar to that proposed for traditional metal oxide non-Ohmic devices, according to similarities discussed herein. (c) 2006 American Institute of Physics.

Type Systems for Distributed Programs: Components and Sessions

Modern software systems, in particular distributed ones, are everywhere around us and are at the basis of our everyday activities. Hence, guaranteeing their cor- rectness, consistency and safety is of paramount importance. Their complexity makes the verification of such properties a very challenging task. It is natural to expect that these systems are reliable and above all usable. i) In order to be reliable, compositional models of software systems need to account for consistent dynamic reconfiguration, i.e., changing at runtime the communication patterns of a program. ii) In order to be useful, compositional models of software systems need to account for interaction, which can be seen as communication patterns among components which collaborate together to achieve a common task. The aim of the Ph.D. was to develop powerful techniques based on formal methods for the verification of correctness, consistency and safety properties related to dynamic reconfiguration and communication in complex distributed systems. In particular, static analysis techniques based on types and type systems appeared to be an adequate methodology, considering their success in guaranteeing not only basic safety properties, but also more sophisticated ones like, deadlock or livelock freedom in a concurrent setting. The main contributions of this dissertation are twofold. i) On the components side: we design types and a type system for a concurrent object-oriented calculus to statically ensure consistency of dynamic reconfigurations related to modifications of communication patterns in a program during execution time. ii) On the communication side: we study advanced safety properties related to communication in complex distributed systems like deadlock-freedom, livelock- freedom and progress. Most importantly, we exploit an encoding of types and terms of a typical distributed language, session π-calculus, into the standard typed π- calculus, in order to understand their expressive power.