A Logic and tool for local reasoning about security protocols

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

Supporting NAT traversal and secure communications in a protocol implementation framework

Dissertação apresentada na Faculdade de Ciências e Tecnologia da Universidade Nova de Lisboa para obtenção do Grau de Mestre em Engenharia Electrotécnica e de Computadores

The African studies course of the Instituto de Estudos Superiores Militares. An analysis of the correlations and conflictive character inside the triangle - Development, environment and security - in Africa’s Nigeria

Relatório de Estágio de Mestrado em Ciência Política e Relações Internacionais Globalização e Ambiente

The impact of large-scale mortgage backed security purchases

A Work Project, presented as part of the requirements for the Award of a Masters Degree in Finance from the NOVA – School of Business and Economics

The impacts of the Cape Verde self-employed social security scheme

A Work Project, presented as part of the requirements for the Award of a Masters Degree in Economics from the NOVA – School of Business and Economics

Intrusion tolerant routing with data consensus in wireless sensor networks

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

Efeitos da laqueação proximal dos vasos curtos e da fundoplicatura total sobre a microcirculação do fundo gástrico : estudo microvascular em cobaias

RESUMO: A operação de Nissen, por laparoscopia, é considerada a cirurgia antirefluxo mais adequada por ser a que melhor replica a fisiologia normal da válvula gastresofágica na maioria dos doentes com sintomas típicos de doença do refluxo gastresofágico (DRGE). São critérios técnicos o encerramento seguro dos pilares do diafragma e a criação de fundoplicatura completa (360 graus), curta (inferior a dois centímetros), lassa e sem tensão – desiderando para o qual a laqueação proximal dos vasos curtos gástricos é crucial. Realizei a operação de Nissen, por laparoscopia, em sessenta mulheres e quarenta homens com DRGE, sem mortalidade operatória, no Serviço de Cirurgia 6 do Hospital dos Capuchos, CHLC, EPE. Os cem doentes apresentavam média etária de 46 anos e queixas, com tempo de evolução entre 1 e 43 anos, de pirose (90%), regurgitação (80%), azia (73%), epigastralgias (54%). A endoscopia alta revelou esofagite de grau Savary-Miller 0-I (62%), II (23%), III (8%), IV (7%); hérnia de deslizamento (71%), hérnia paraesofágica (8%), sem hérnia (21%); a pHmetria de 24h diagnosticou padrão misto (38%), levantado (20%), deitado (20%), inconclusiva (22%) e a manometria diagnosticou EEI hipotónico (35%), peristálise esofágica normal (88%), hipomotilidade ligeira (5%) e foi omissa (7%). Hérnia hiatal, esofagite grave, ineficácia do controlo sintomático com inibidor da bomba de protões e desejo de descontinuidade terapêutica constituíram as indicações para tratamento cirúrgico. Por celioscopia, efetuei laqueação dos vasos curtos gástricos (70%), cruroplastia e fundoplicatura total (seda 2/0), curta (dimensão média 1,5-2 cm), lassa, sem tensão e sem calibração intraoperatória do esófago. A fundoplicatura de Nissen laparoscópica mostrou-se segura e eficaz no tratamento da DRGE. A sua idoneidade foi ainda comprovada pela normalização da pHmetria de 24 horas e da manometria pós-operatórias, com significado estatístico, num grupo de catorze voluntários assintomáticos. Em catamnese com recuo médio 30,7 meses 94% dos indivíduos persistem assintomáticos. Interrogando-me acerca das repercussões desta operação sobre a microcirculação do fundo gástrico coloquei, como premissa, a possibilidade de na operação de Nissen a laqueação dos vasos curtos poder induzir modificação no diâmetro arteriolar da parede do fundo gástrico. Para pesquisar a influência da laqueação dos vasos curtos gástricos e da fundoplicatura total sobre o calibre arteriolar da parede do estômago no cárdia, no fundo e na região dos vasos curtos gástricos, idealizei um Projeto de investigação experimental em cobaias. O Projeto foi desenvolvido no Centro de Investigação do Departamento de Anatomia da FCM-UNL. Para a sua realização obtive autorização da Comissão Científica e Pedagógica da FCM-UNL, requeri a acreditação como investigador à Direção Geral de Veterinária e, por recorrer à utilização de animais, submeti-o à Comissão de Ética da FCM-UNL, que o aprovou por unanimidade. Para limitar o número de animais utilizados ao mínimo necessário, calculei, por método estatístico, a quantidade de cobaias necessárias. Subdividindo-as num grupo de ensaio (GE), onde realizei a operação de Nissen, e num grupo de controlo (GC), onde apenas procedi a tração gástrica, defini e apliquei protocolos de anestesia, de cirurgia e de eutanásia, segundo os princípios dos 3R – Replacement, Reduction, Refinement da técnica de experimentação humana de Russell e Burch (1959) – uma estrutura ética amplamente aceite para a realização de experimentação científica humanizada com animais. A utilização das técnicas de estudo angiomorfológico permitiu-me analisar e descrever a anatomia normal, a vascularização arterial macroscópica, a microangioarquitetura, por microscopia eletrónica de varrimento de moldes de corrosão vascular, e a histologia da parede do estômago da cobaia. Procedi, também, à definição dos critérios morfológicos que considerei suscetíveis de validação deste modelo animal para o estudo proposto. Por razões académicas, foi necessário abreviar o Projeto encurtando, em cerca de dois anos, o prazo disponível para conclusão do estudo. Apreciando-o com o Gabinete de Análise Epidemiológica e Estatística do Centro de Investigação do CHLC, EPE, optou-se, perante a escassez de elementos após já terem sido recrutados 46 animais, por uma amostra, suplementar, de dimensão de conveniência de oito cobaias (quatro em cada grupo), condicionada pelo limite temporal universitário e pelo respeito pela dignidade dos animais. Neste subgrupo procedi, por microscopia eletrónica de varrimento, à medição dos calibres arteriolares nos moldes vasculares do cárdia, do fundo e da zona dos vasos curtos gástricos tanto no GC como no GE efetuando 469 medições no primeiro e 461 no último. Os dados foram enviados ao Centro de Investigação do CHLC, EPE que procedeu à sua análise estatística (ANOVA). A referida análise revelou que as arteríolas do plexo mucoso e as do plexo submucoso do cárdia, do fundo e da região dos vasos curtos gástricos, mostraram aumento de calibre no GE. O aumento foi, estatisticamente, significativo por ser superior a 50% do calibre do GC. Nos vasos curtos, a diferença foi mais pequena, mas persistiu sendo, estatisticamente, significativa. Os vasos retos dilataram na base, na sua emergência do plexo seroso, apenas no fundo gástrico. Na cobaia a operação de Nissen – fundoplicatura total com laqueação dos vasos curtos gástricos –, provocou vasodilatação arteriolar do fundo gástrico. Considero que essa vasodilatação constituiu acomodação à modificação introduzida e infiro que o mesmo possa acontecer no ser humano. Admito, assim, que também ocorra vasodilatação no ser humano, na sequência da laqueação dos vasos curtos gástricos, pela analogia microvascular entre as duas espécies e que essa vasodilatação corresponda, igualmente, a um mecanismo de adaptação arteriolar visando, por exemplo, suprir a perda incorrida pela laqueação. A associação experimental entre laqueação dos vasos curtos gástricos e realização de fundoplicatura total, que exerce aumento inerente de pressão sobre a JEG, não só não provocou défice da microcirculação do esófago distal ou do estômago proximal como desencadeou um mecanismo de vasodilatação fúndica que reforça o conceito de segurança da operação de Nissen para tratamento da DRGE. -------------- ABSTRACT: The laparoscopic Nissen operation is considered to be the most appropriate antirefluxsurgery because it suitably replicates the standard physiology of the gastroesophageal valve in most patients with typical symptoms of gastroesophageal reflux disease (GERD). The technical criteria includes the safe shutdown of the diafragmatic crura(cruroplasty) and the creation of a complete fundoplication (360 degrees), short (lesser than two inches), floppy and without tension – a goal for which the proximal ligation of the gastric short vessels is crucial. The laparoscopic Nissen operation was performed in sixty women and forty men with GERD, without any operative mortality, at the Surgical Department of the Hospital dos Capuchos, CHLC, EPE. The one hundred patients, averaged 46 years old, complained of heartburn (90%), regurgitation (80%) and upper abdominal pain (54 %). The endoscopy process revealed Savary-Miller esophagitis of grade 0-I (62%), II (23%), III (8%), IV (7%), sliding hernia (71%), paraesophageal hernia (8%) or no herniation (21%). The pHmetry/24h diagnosed mixed pattern (38%), raised (20%), lying (20%) or inconclusive (22%). The manometry diagnosed hypotensive LES (35%), normal esophageal peristalsis (88%), mild hypomotility (5%) and was absent (7%). Hiatal hernia, severe esophagitis, ineffective symptomatic control with proton pump inhibitor and request for treatment discontinuation were the signs for surgical action. A laparoscopic ligation of short gastric vessels (70%), cruroplasty and fundoplication (silk 2/0), short (average size 1.5–2 cm) and floppy, without tension and without intraoperative calibration of the esophagus were thus performed. The laparoscopic Nissen fundoplication behaved safe and effective in treating GERD. In a group of 14 asymptomatic volunteers its reputation was confirmed with statistical significance by normalization of postoperative pHmetry/24h and manometry. 94% of the individuals remained asymptomatic up to 30.7 months (average) in the follow-up. Interrogating myself about the impact of this operation on the microcirculation of the gastric fundus I put premised on the possibility of the ligation of the short gastric vessels in the Nissen procedure can induce changes in the arteriolar diameter in the Wall of the gastric fundus. To explore the influence of ligation of the short gastric vessels and the fundoplication at the arteriolar caliber of the cardia, the fundus and the region of the short vessels of the gastric wall, I designed a project of experimental research in guinea pigs with two interdependent components: one veterinary and another technical where I applied angiomorphological studies. The project was developed at the Research Centre of the Department of Anatomy FCMUNL. For its accomplishment I got permission from the Scientific and Pedagogical Committee of the FCM-UNL, I requested for accreditation as a researcher at the General Directorate of Veterinary and, by resorting to the use of animals I submitted it to the Ethics Committee of the FCM-UNL, which approved it unanimously. The guinea pigs were divided into two experimental groups: an experimental group (EG), in which the Nissen procedure was performed and a control group (CG) in which only a gastric traction was done. Protocols of anesthesia, surgery and euthanasia were applied according to the 3Rs – Replacement, Reduction, Refinement of the technique of human experimentation of Burch and Russell (1959) – a widely accepted ethical framework for conducting scientific experiments using animals humanely. Using histological and angiomorphological techniques, I performed the analysis and the description of the normal, macro and microvascular, anatomy of the guinea pig stomach and I defined the morphological criteria that I considered susceptible for validation of this animal model for the proposed study. By means of scanning electron microscopy I measured the arteriolar calibers of the vascular casts of the cardia, of the fundus and of the short gastric vessels in both CG and EG, making 469 measurements in the former and 461 in the latter. The data were sent to the Research Center of the CHLC which conducted the statistical analysis (ANOVA). The data were sent to the Centre for Research of the CHLC, EPE which proceeded to statistical analysis (ANOVA). This analysis revealed that the arterioles plexus of the mucosal and submucosal plexus of the cardia, fundus and region of the short gastric vessels, showed increased caliber in EG. The increase was statistically significant for being greater than 50% CG gauge. In the short gastric vessels, the difference was smaller, but persisted and statistically significant. Straight vessels were dilated at the base, on its emergence of the plexus serous only in the fundus. In the guinea pig, the Nissen procedure - complete fundoplication with ligation of the short gastric vessels - caused arteriolar vasodilation on the gastric fundus. I believe that this vasodilation constituted some accommodation to the modification introduced and infer that the same might happen in humans. I admit therefore that vasodilation also occurs in humans following the ligation of the short gastric vessels by microvascular analogy between the two species and that this vasodilation corresponds also to na adaptation mechanism arteriolar, for example, to compensate the loss incurred by ligation. The association of experimental ligation of the short gastric vessels with conducting complete fundoplication, which exerts increased pressure on the EGJ, not only did not cause a microcirculation deficit of the distal esophagus or proximal stomach as triggered a mechanism of fundic vasodilation which reinforces the security concept of the Nissen procedure for treatment of GERD.

Planning and verification of multipath routing protocols

Conventionally the problem of the best path in a network refers to the shortest path problem. However, for the vast majority of networks present nowadays this solution has some limitations which directly affect their proper functioning, as well as an inefficient use of their potentialities. Problems at the level of large networks where graphs of high complexity are commonly present as well as the appearing of new services and their respective requirements, are intrinsically related to the inability of this solution. In order to overcome the needs present in these networks, a new approach to the problem of the best path must be explored. One solution that has aroused more interest in the scientific community considers the use of multiple paths between two network nodes, where they can all now be considered as the best path between those nodes. Therefore, the routing will be discontinued only by minimizing one metric, where only one path between nodes is chosen, and shall be made by the selection of one of many paths, thereby allowing the use of a greater diversity of the present paths (obviously, if the network consents). The establishment of multi-path routing in a given network has several advantages for its operation. Its use may well improve the distribution of network traffic, improve recovery time to failure, or it can still offer a greater control of the network by its administrator. These factors still have greater relevance when networks have large dimensions, as well as when their constitution is of high complexity, such as the Internet, where multiple networks managed by different entities are interconnected. A large part of the growing need to use multipath protocols is associated to the routing made based on policies. Therefore, paths with different characteristics can be considered with equal level of preference, and thus be part of the solution for the best way problem. To perform multi-path routing using protocols based only on the destination address has some limitations but it is possible. Concepts of graph theory of algebraic structures can be used to describe how the routes are calculated and classified, enabling to model the routing problem. This thesis studies and analyzes multi-path routing protocols from the known literature and derives a new algebraic condition which allows the correct operation of these protocols without any network restriction. It also develops a range of software tools that allows the planning and the respective verification/validation of new protocols models according to the study made.

Maritime Security in the Gulf of Guinea: Issues and Solutions for the 21st Century

A producer of 5.4 M bbl/d, totalling almost half of the consumption of the entire European Union, the Gulf of Guinea is a fundamental lifeline and maritime link between Europe, the Americas and Africa. Geographically positioned as a staging post for transit originating in Latin America and coupled with its relatively porous borders, the region is also the perfect stepping stone for contraband heading to European shores. While blessed with an enviable wealth of marine and mineral resources, the region is also plagued by an ever-increasing spectre of maritime piracy; accounting for around 30% of incidents in African waters from 2003 to 2011. It is for these reasons that this research centres around the issues of maritime security in the Gulf of Guinea, with a particular focus on the first two decades of the 21st century. This research looks to examine the overall picture of the present state of play in the area, before going on to provide an analysis of potential regional developments in maritime security. This research begins with the analysis of concepts/phenomena that have played a notable role in the shaping of the field of maritime security, namely Globalisation and security issues in the post-Cold War era. The ensuing chapter then focuses in on the Gulf of Guinea and the issues dominating the field of maritime security in the region. The penultimate chapter presents a SWOT analysis, undertaken as part of this research with the aim of correlating opinions from a variety of sectors/professions regarding maritime security in the Gulf of Guinea. The final chapter builds upon the results obtained from the abovementioned SWOT analysis, presenting a series of potential proposals/strategies that can contribute to the field of maritime security in the region over the coming years. This research draws to a close with the presentation of conclusions taken from this particular investigation, as well as a final overview of the earlier presented proposals applicable to the field of maritime security during the second decade of the 21st century.

AGNI: an API for the control of automomous service robots

With the continuum growth of Internet connected devices, the scalability of the protocols used for communication between them is facing a new set of challenges. In robotics these communications protocols are an essential element, and must be able to accomplish with the desired communication. In a context of a multi-­‐‑agent platform, the main types of Internet communication protocols used in robotics, mission planning and task allocation problems will be revised. It will be defined how to represent a message and how to cope with their transport between devices in a distributed environment, reviewing all the layers of the messaging process. A review of the ROS platform is also presented with the intent of integrating the already existing communication protocols with the ServRobot, a mobile autonomous robot, and the DVA, a distributed autonomous surveillance system. This is done with the objective of assigning missions to ServRobot in a security context.

Determinants of social security pensions expenditure in Portugal

In most European countries Social Security (SS) systems are characterized as Pay-asyou- go systems. Their sustainability is being challenged with demographic changes, namely population ageing. Portugal’s population is ageing rapidly being one of the countries where this problem is more critical. With the growing debate on this topic several public choice models have been developed so as to explain SS size. In this work project there is an attempt to understand whether these models contribute to better explain Social security expenditure with pensions (SSEP) and to establish the need of finding ways to reduce present commitment with pension expenditure in Portugal.

Future lending income and security value

I test the Duffie, Gârleanu, and Pedersen hypothesis that security prices incorporate expected future securities lending income. To determine whether institutional investors anticipate gains from future lending of securities, I examine their trading behavior around loan-fee increases. The evidence suggests that institutions buy shares in response to an increase in lending fees, and that this could explain the premium associated with high- lending-fee stocks. Expected future lending income affects stock prices, although the effect seems to be attenuated by the negative information that arises from short selling.

A wave of change: Labor market and social security impacts of the EU refugee inflow

The recent massive inflow of refugees to the European Union (EU) raises a number of unanswered questions on the economic impact of this phenomenon. To examine these questions, we constructed an overlapping-generations model that describes the evolution of the skill premium and of the welfare benefit level in relevant European countries, in the aftermath of an inflow of asylum-seekers. In our simulation, relative wages of skilled workers increase between 8% and 11% in the period of the inflow; their subsequent time path is dependent on the initial skill premium. The entry of migrants creates a fiscal surplus of about 8%, which can finance higher welfare benefits in the subsequent periods. These effects are weaker in a scenario where refugees do not fully integrate into the labor market.

Rely-guarantee protocols for safe interference over shared memory

Mutable state can be useful in certain algorithms, to structure programs, or for efficiency purposes. However, when shared mutable state is used in non-local or nonobvious ways, the interactions that can occur via aliases to that shared memory can be a source of program errors. Undisciplined uses of shared state may unsafely interfere with local reasoning as other aliases may interleave their changes to the shared state in unexpected ways. We propose a novel technique, rely-guarantee protocols, that structures the interactions between aliases and ensures that only safe interference is possible. We present a linear type system outfitted with our novel sharing mechanism that enables controlled interference over shared mutable resources. Each alias is assigned separate, local roles encoded in a protocol abstraction that constrains how an alias can legally use that shared state. By following the spirit of rely-guarantee reasoning, our rely-guarantee protocols ensure that only safe interference can occur but still allow many interesting uses of shared state, such as going beyond invariant and monotonic usages. This thesis describes the three core mechanisms that enable our type-based technique to work: 1) we show how a protocol models an alias’s perspective on how the shared state evolves and constrains that alias’s interactions with the shared state; 2) we show how protocols can be used while enforcing the agreed interference contract; and finally, 3) we show how to check that all local protocols to some shared state can be safely composed to ensure globally safe interference over that shared memory. The interference caused by shared state is rooted at how the uses of di↵erent aliases to that state may be interleaved (perhaps even in non-deterministic ways) at run-time. Therefore, our technique is mostly agnostic as to whether this interference was the result of alias interleaving caused by sequential or concurrent semantics. We show implementations of our technique in both settings, and highlight their di↵erences. Because sharing is “first-class” (and not tied to a module), we show a polymorphic procedure that enables abstract compositions of protocols. Thus, protocols can be specialized or extended without requiring specific knowledge of the interference produce by other protocols to that state. We show that protocol composition can ensure safety even when considering abstracted protocols. We show that this core composition mechanism is sound, decidable (without the need for manual intervention), and provide an algorithm implementation.