Development of composite particles for pulmonary delivery

In this work, biocompatible and biodegradable poly(D-L-lactide-co-glycolide) (PLGA) microparticles with the potential for use as a controlled release system of vaccines and other drugs to the lung were manufactured using supercritical CO2, through the Supercritical Assisted Atomization (SAA) technique. After performing a controlled variance in production parameters (temperature, pressure, CO2/solution flow ratio) PLGA microparticles were characterized and later used to encapsulate active pharmaceutical ingredients (API). Bovine serum albumin (BSA) was chosen as model protein and vaccine, while sildenafil was the chosen drug to treat pulmonary artery hypertension and their effect on the particles characteristics was evaluated. All the produced formulations were characterized in relation to their morphology (Morphologi G3 and scanning electronic microscopy (SEM)), to their physical-chemical properties (X-ray diffraction (XRD, differential scanning calorimetry (DSC), Fourier transform infrared (FTIR)) and aerodynamic performance using an in vitro aerosolization study – Andersen cascade impactor (ACI) - to obtain data such as the fine particle fraction (FPF) and the mass median aerodynamic diameter (MMAD). Furthermore, pharmacokinetic, biodegradability and biocompatibility tests were performed in order to verify the particle suitability for inhalation. The resulting particles showed aerodynamic diameters between the 3 and 5 μm, yields up to 58% and FPF percentages rounding the 30%. Taken as a whole, the produced microparticles do present the necessary requests to make them appropriate for pulmonary delivery.

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