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

Sistemas de Tipos para Verificación de Programas Concurrentes. Type Systems for Concurrent Programs Verification.

La programación concurrente es una tarea difícil aún para los más experimentados programadores. Las investigaciones en concurrencia han dado como resultado una gran cantidad de mecanismos y herramientas para resolver problemas de condiciones de carrera de datos y deadlocks, problemas que surgen por el mal uso de los mecanismos de sincronización. La verificación de propiedades interesantes de programas concurrentes presenta dificultades extras a los programas secuenciales debido al no-determinismo de su ejecución, lo cual resulta en una explosión en el número de posibles estados de programa, haciendo casi imposible un tratamiento manual o aún con la ayuda de computadoras. Algunos enfoques se basan en la creación de lenguajes de programación con construcciones con un alto nivel de abstración para expresar concurrencia y sincronización. Otros enfoques tratan de desarrollar técnicas y métodos de razonamiento para demostrar propiedades, algunos usan demostradores de teoremas generales, model-checking o algortimos específicos sobre un determinado sistema de tipos. Los enfoques basados en análisis estático liviano utilizan técnicas como interpretación abstracta para detectar ciertos tipos de errores, de una manera conservativa. Estas técnicas generalmente escalan lo suficiente para aplicarse en grandes proyectos de software pero los tipos de errores que pueden detectar es limitada. Algunas propiedades interesantes están relacionadas a condiciones de carrera y deadlocks, mientras que otros están interesados en problemas relacionados con la seguridad de los sistemas, como confidencialidad e integridad de datos. Los principales objetivos de esta propuesta es identificar algunas propiedades de interés a verificar en sistemas concurrentes y desarrollar técnicas y herramientas para realizar la verificación en forma automática. Para lograr estos objetivos, se pondrá énfasis en el estudio y desarrollo de sistemas de tipos como tipos dependientes, sistema de tipos y efectos, y tipos de efectos sensibles al flujo de datos y control. Estos sistemas de tipos se aplicarán a algunos modelos de programación concurrente como por ejemplo, en Simple Concurrent Object-Oriented Programming (SCOOP) y Java. Además se abordarán propiedades de seguridad usando sistemas de tipos específicos. Concurrent programming has remained a dificult task even for very experienced programmers. Concurrency research has provided a rich set of tools and mechanisms for dealing with data races and deadlocks that arise of incorrect use of synchronization. Verification of most interesting properties of concurrent programs is a very dificult task due to intrinsic non-deterministic nature of concurrency, resulting in a state explosion which make it almost imposible to be manually treat and it is a serious challenge to do that even with help of computers. Some approaches attempts create programming languages with higher levels of abstraction for expressing concurrency and synchronization. Other approaches try to develop reasoning methods to prove properties, either using general theorem provers, model-checking or specific algorithms on some type systems. The light-weight static analysis approach apply techniques like abstract interpretation to find certain kind of bugs in a conservative way. This techniques scale well to be applied in large software projects but the kind of bugs they may find are limited. Some interesting properties are related to data races and deadlocks, while others are interested in some security problems like confidentiality and integrity of data. The main goals of this proposal is to identify some interesting properties to verify in concurrent systems and develop techniques and tools to do full automatic verification. The main approach will be the application of type systems, as dependent types, type and effect systems, and flow-efect types. Those type systems will be applied to some models for concurrent programming as Simple Concurrent Object-Oriented Programming (SCOOP) and Java. Other goals include the analysis of security properties also using specific type systems.

L-Fuzzy Relations in Coq

Heyting categories, a variant of Dedekind categories, and Arrow categories provide a convenient framework for expressing and reasoning about fuzzy relations and programs based on those methods. In this thesis we present an implementation of Heyting and arrow categories suitable for reasoning and program execution using Coq, an interactive theorem prover based on Higher-Order Logic (HOL) with dependent types. This implementation can be used to specify and develop correct software based on L-fuzzy relations such as fuzzy controllers. We give an overview of lattices, L-fuzzy relations, category theory and dependent type theory before describing our implementation. In addition, we provide examples of program executions based on our framework.

A Compiler for the dependently typed language Beluga

Les structures avec des lieurs sont très communes en informatique. Les langages de programmation et les systèmes logiques sont des exemples de structures avec des lieurs. La manipulation de lieurs est délicate, de sorte que l’écriture de programmes qui ma- nipulent ces structures tirerait profit d’un soutien spécifique pour les lieurs. L’environ- nement de programmation Beluga est un exemple d’un tel système. Nous développons et présentons ici un compilateur pour ce système. Parmi les programmes pour lesquels Beluga est spécialement bien adapté, plusieurs peuvent bénéficier d’un compilateur. Par exemple, les programmes pour valider les types (les "type-checkers"), les compilateurs et les interpréteurs tirent profit du soutien spécifique des lieurs et des types dépendants présents dans le langage. Ils nécessitent tous également une exécution efficace, que l’on propose d’obtenir par le biais d’un compilateur. Le but de ce travail est de présenter un nouveau compilateur pour Beluga, qui emploie une représentation interne polyvalente et permet de partager du code entre plusieurs back-ends. Une contribution notable est la compilation du filtrage de Beluga, qui est particulièrement puissante dans ce langage.

Costruzioni modulari in linguaggi con tipi dipendenti.

In questa tesi si indaga come è possibile strutturare in modo modulare programmi e prove in linguaggi con tipi dipendenti. Il lavoro è sviluppato nel linguaggio di programmazione con tipi dipendenti Agda. Il fine è quello di tradurre l'approccio Datatypes à la carte, originariamente formulato per Haskell, in Type Theory: puntiamo ad ottenere un simile embedding di una nozione di sottotipaggio per tipi ricorsivi, che permetta sia la definizione di programmi con side-effect dove i diversi effetti sono definiti modularmente, che la modularizzazione di sintassi, semantica e ragionamento relativi a descrizioni di linguaggi.

Hormones and mammary carcinogenesis in mice, rats, and humans: a unifying hypothesis.

An attempt has been made to put forward a unifying hypothesis explaining the role hormones play in the genesis of mammary cancers of different phenotypes and genotypes in mice, rats, and humans. Most mammary cancers in these species originate in luminal mammary epithelial cells lining the mammary ducts and alveoli. These cancers are histopathologically diverse and are classified on the basis of growth requirements as hormone-dependent or hormone-independent tumors. In most strains of mice, mammary cancers at the time of detection are largely of the hormone-independent type; in rats, almost all mammary cancers are hormone-dependent, while humans have both phenotypes. In spite of these differences, in vivo studies show that hormones (ovarian and pituitary) are essential for luminal mammary epithelial cell proliferation and also for the development of mammary cancers of both hormone-independent and hormone-dependent types. This article, based on our extensive in vivo and in vivo studies and on current literature, proposes a model to explain the central role of hormones in the genesis of all types of mammary cancers. The model attempts to address the following questions: (i) how hormones regulate luminal mammary epithelial cell proliferation, (ii) why hormones are required for the genesis of mammary cancers of all phenotypes and genotypes, including those which are always classified as hormone-independent tumors, and (iii) why the three species (mouse, rat, and human) have consistently different ratios of hormone-dependent to hormone-independent tumors.

Quantitative Intercellular Localization of NADH-Dependent Glutamate Synthase Protein in Different Types of Root Cells in Rice Plants1

The quantitative analysis with immunogold-electron microscopy using a single-affinity-purified anti-NADH-glutamate synthase (GOGAT) immunoglobulin G (IgG) as the primary antibody showed that the NADH-GOGAT protein was present in various forms of plastids in the cells of the epidermis and exodermis, in the cortex parenchyma, and in the vascular parenchyma of root tips (<10 mm) of rice (Oryza sativa) seedlings supplied with 1 mm NH4+ for 24 h. The values of the mean immunolabeling density of plastids were almost equal among these different cell types in the roots. However, the number of plastids per individual cell type was not identical, and some parts of the cells in the epidermis and exodermis contained large numbers of plastids that were heavily immunolabeled. Although there was an indication of labeling in the mitochondria using the single-affinity-purified anti-NADH-GOGAT IgG, this was not confirmed when a twice-affinity-purified IgG was used, indicating an exclusively plastidial location of the NADH-GOGAT protein in rice roots. These results, together with previous work from our laboratory (K. Ishiyama, T. Hayakawa, and T. Yamaya [1998] Planta 204: 288–294), suggest that the assimilation of exogeneously supplied NH4+ ions is primarily via the cytosolic glutamine synthetase/plastidial NADH-GOGAT cycle in specific regions of the epidermis and exodermis in rice roots. We also discuss the role of the NADH-GOGAT protein in vascular parenchyma cells.

A Limit Theorem for Multi-Type Subcritical Age-Dependent Branching Processes with two Types of Immigration

Марусия Н. Славчова-Божкова - В настоящата работа се обобщава една гранична теорема за докритичен многомерен разклоняващ се процес, зависещ от възрастта на частиците с два типа имиграция. Целта е да се обобщи аналогичен резултат в едномерния случай като се прилагат “coupling” метода, теория на възстановяването и регенериращи процеси.

Low-Level Laser Irradiation (InGaAlP-660 nm) Increases Fibroblast Cell Proliferation and Reduces Cell Death in a Dose-Dependent Manner

Background and Objective: Impaired cell metabolism and increased cell death in fibroblast cells are physiological features of chronic tendinopathy. Although several studies have shown that low-level laser therapy (LLLT) at certain parameters has a biostimulatory effect on fibroblast cells, it remains uncertain if LLLT effects depend on the physiological state. Study Design/Material and Methods: High-metabolic immortal cell culture and primary human keloid fibroblast cell culture were used in this study. Trypan blue exclusion and the 3-(4,5-dimethylthiazol-2-yl)-2,5-diphenyltetrazolium bromide (MTT) test were used to determine cell viability and proliferation. Propidium iodide stain was used for cell-cycle analysis by flow cytometry. Laser irradiation was performed daily on three consecutive days with a GaAlAs 660-nm laser (mean output: 50 mW, spot size 2 mm(2), power density = 2.5 W/cm(2)) and a typical LLLT dose and a high LLLT dose (irradiation times: 60 or 420 s; fluences: 150 or 1050 J/cm(2); energy delivered: 3 or 21 J). Results: Primary fibroblast cell culture from human keloids irradiated with 3 J showed significant proliferation by the trypan blue exclusion test (p < 0.05), whereas the 3T3 cell culture showed no difference using this method. Propidium iodide staining flow cytometry data showed a significant decrease in the percentage of cells being in proliferative phases of the cell cycle (S/g(2)/M) when irradiated with 21 J in both cell types (hypodiploid cells increased). Conclusions: Our data support the hypothesis that the physiological state of the cells affects the LLLT results, and that high-metabolic rate and short-cell-cycle 3T3 cells are not responsive to LLLT. In conclusion, LLLT with a dose of 3 J reduced cell death significantly, but did not stimulate cell cycle. A LLLT dose of 21 J had negative effects on the cells, as it increased cell death and inhibited cell proliferation.

Response surface methodology applied to SPE for the determination of ibuprofen in various types of water samples

Over the last few years, there has been a growing concern about the presence of pharmaceuticals in the environment. The main objective of this study was to develop and validate an SPE method using surface response methodology for the determination of ibuprofen in different types of water samples. The influence of sample pH and sample volume on the ibuprofen recovery was studied. The effect of each studied independent variable is pronounced on the dependent variable (ibuprofen recovery). Good selectivity, extraction efficiency, and precision were achieved using 600 mL of sample volume with the pH adjusted to 2.2. LC with fluorescence detection was employed. The optimized method was applied to 20 water samples from the North and South of Portugal.

Activity-Dependent Neurorehabilitation Beyond Physical Trainings: "Mental Exercise" Through Mirror Neuron Activation

The activity dependent brain repair mechanism has been widely adopted in many types of neurorehabilitation. The activity leads to target specific and non-specific beneficial effects in different brain regions, such as the releasing of neurotrophic factors, modulation of the cytokines and generation of new neurons in adult hood. However physical exercise program clinically are limited to some of the patients with preserved motor functions; while many patients suffered from paralysis cannot make such efforts. Here the authors proposed the employment of mirror neurons system in promoting brain rehabilitation by "observation based stimulation". Mirror neuron system has been considered as an important basis for action understanding and learning by mimicking others. During the action observation, mirror neuron system mediated the direct activation of the same group of motor neurons that are responsible for the observed action. The effect is clear, direct, specific and evolutionarily conserved. Moreover, recent evidences hinted for the beneficial effects on stroke patients after mirror neuron system activation therapy. Finally some music-relevant therapies were proposed to be related with mirror neuron system.

The role of Pep4p, the vacuolar yeast protease ortholog of human cathepsin D, in mitochondria-dependent apoptosis

Doctoral Thesis (PhD Programm on Molecular and Environmental Biology)

Evaluation of inflammatory response induced by different types of daily contact lenses

Dissertação de mestrado em Genética Molecular

Tissue-specific segregation of CD1d-dependent and CD1d-independent NK T cells.

NKT cells, defined as T cells expressing the NK cell marker NK1.1, are involved in tumor rejection and regulation of autoimmunity via the production of cytokines. We show in this study that two types of NKT cells can be defined on the basis of their reactivity to the monomorphic MHC class I-like molecule CD1d. One type of NKT cell is positively selected by CD1d and expresses a biased TCR repertoire together with a phenotype found on activated T cells. A second type of NKT cell, in contrast, develops in the absence of CD1d, and expresses a diverse TCR repertoire and a phenotype found on naive T cells and NK cells. Importantly, the two types of NKT cells segregate in distinct tissues. Whereas thymus and liver contain primarily CD1d-dependent NKT cells, spleen and bone marrow are enriched in CD1d-independent NKT cells. Collectively, our data suggest that recognition of tissue-specific ligands by the TCR controls localization and activation of NKT cells.