Abstraction-carrying code: a model for mobile code safety

Proof-Carrying Code (PCC) is a general approach to mobile code safety in which programs are augmented with a certificate (or proof). The intended benefit is that the program consumer can locally validate the certificate w.r.t. the "untrustcd" program by means of a certificate checker a process which should be much simpler, efficient, and automatic than generating the original proof. The practical uptake of PCC greatly depends on the existence of a variety of enabling technologies which allow both proving programs correct and replacing a costly verification process by an efficient checking proceduri on th( consumer side. In this work we propose Abstraction- Carrying Code (ACC), a novel approach which uses abstract interpretation as enabling technology. We argue that the large body of applications of abstract interpretation to program verification is amenable to the overall PCC scheme. In particular, we rely on an expressive class of safely policies which can be defined over different abstract domains. We use an abstraction (or abstract model) of the program computed by standard static analyzers as a certificate. The validity of the abstraction on ihe consumer side is checked in a single pass by a very efficient and specialized abstract-interpreter. We believe that ACC brings the expressiveness, flexibility and automation which is inherent in abstract interpretation techniques to the area of mobile code safety.

Comparison of CO2 from coal captureprocesses and valorisation technologies

Coal is the most plentiful and evenly distributed fossil fuel worldwide. Based on current production, it is estimated that the reserves will last approximately 130 years. Its use worldwide has been increasing, mainly due to consumption by emerging countries. CO2 emissions generated by combustion and the repercussions of such on climate change support the view that it could no longer be used. CO2 capture may be the solution to continue using it, which would cater for the growing energy demand worldwide. The aim of this study is to compare different processes concerning CO2 capture that may be economically viable, ultimately showing that coal, a fossil energy source widely distributed around the world, can, as a result of using different CO2 capture processes, be used as a clean source of electricity. Hence, in places where geological hurdles may render the costs of CO2 storage considerably higher, since it might have to travel far, coal may be used for other purposes, thus valorizing CO2 within the industrial sector. This research is focused on the technical and economic comparison of the most relevant CO2 capture projects designed in Spain using different existing technologies. The oxyfuel project in Ciuden (Leon, Spain), the IGCC Elcogas, precombustion CO2-capture project (Puertollano, Spain) and the postcombustion project in Carboneras (Almeria, Spain) will be analyzed in order to assess the options available to valorizecaptured CO2. Valorizing captured CO2 may be an adequate solution in areas where, although CO2 capture is still possible, storage is not equally so, thus generating a further benefit. The possible uses of CO2 will be assessed in vegetable growing greenhouses, harnessing CO2 in vegetable life cycles. This will also be used in growing algae for subsequent biodiesel production. Both CO2capture and valorizing will eventually lead to the clean use of coal, which will thus enhance the level of self-supply, aiding the development of electric vehicles, which require large amounts of electricity, as well as improve the level of energy autonomy in countries around the world. Another type of fuel, biodiesel, will also be obtained, without this affecting international food prices.

Abstraction-carrying code

Proof-Carrying Code (PCC) is a general approach to mobile code safety in which programs are augmented with a certifícate (or proof). The practical uptake of PCC greatly depends on the existence of a variety of enabling technologies which allow both to prove programs correct and to replace a costly verification process by an efñcient checking procedure on the consumer side. In this work we propose Abstraction-Carrying Code (ACC), a novel approach which uses abstract interpretation as enabling technology. We argüe that the large body of applications of abstract interpretation to program verification is amenable to the overall PCC scheme. In particular, we rely on an expressive class of safety policies which can be defined over different abstract domains. We use an abstraction (or abstract model) of the program computed by standard static analyzers as a certifícate. The validity of the abstraction on the consumer side is checked in a single-pass by a very efficient and specialized abstract-interpreter. We believe that ACC brings the expressiveness, flexibility and automation which is inherent in abstract interpretation techniques to the área of mobile code safety. We have implemented and benchmarked ACC within the Ciao system preprocessor. The experimental results show that the checking phase is indeed faster than the proof generation phase, and that the sizes of certificates are reasonable.

Experiments in abstract interpretation-based code certification for pervasive systems

Proof carrying code (PCC) is a general is originally a roof in ñrst-order logic of certain vermethodology for certifying that the execution of an un- ification onditions and the checking process involves trusted mobile code is safe. The baste idea is that the ensuring that the certifícate is indeed a valid ñrst-order code supplier attaches a certifícate to the mobile code proof. which the consumer checks in order to ensure that the The main practical difñculty of PCC techniques is in code is indeed safe. The potential benefit is that the generating safety certiñeates which at the same time: i) consumer's task is reduced from the level of proving to allow expressing interesting safety properties, ii) can be the level of checking. Recently, the abstract interpre- generated automatically and, iii) are easy and efficient tation techniques developed, in logic programming have to check. In [1], the abstract interpretation techniques been proposed as a basis for PCC. This extended ab- [5] developed in logic programming1 are proposed as stract reports on experiments which illustrate several is- a basis for PCC. They offer a number of advantages sues involved in abstract interpretation-based certifica- for dealing with the aforementioned issues. In particution. First, we describe the implementation of our sys- lar, the xpressiveness of existing abstract domains will tem in the context of CiaoPP: the preprocessor of the be implicitly available in abstract interpretation-based Ciao multi-paradigm programming system. Then, by code certification to deñne a wide range of safety propermeans of some experiments, we show how code certifi- ties. Furthermore, the approach inherits the automation catión is aided in the implementation of the framework. and inference power of the abstract interpretation en- Finally, we discuss the application of our method within gines used in (Constraint) Logic Programming, (C)LP. the área, of pervasive systems

Abstract interpretation-based mobile code certification

Current approaches to mobile code safety – inspired by the technique of Proof-Carrying Code (PCC) [4] – associate safety information (in the form of a certificate) to programs. The certificate (or proof) is created by the code supplier at compile time, and packaged along with the untrusted code. The consumer who receives the code+certificate package can then run a checker which, by a straightforward inspection of the code and the certificate, is able to verify the validity of the certificate and thus compliance with the safety policy. The main practical difficulty of PCC techniques is in generating safety certificates which at the same time: i) allow expressing interesting safety properties, ii) can be generated automatically and, iii) are easy and efficient to check.

Abstraction carrying code and resource-awareness

Proof-Carrying Code (PCC) is a general approach to mobile code safety in which the code supplier augments the program with a certifícate (or proof). The intended benefit is that the program consumer can locally validate the certifícate w.r.t. the "untrusted" program by means of a certifícate checker—a process which should be much simpler, eíñcient, and automatic than generating the original proof. Abstraction Carrying Code (ACC) is an enabling technology for PCC in which an abstract model of the program plays the role of certifícate. The generation of the certifícate, Le., the abstraction, is automatically carried out by an abstract interpretation-based analysis engine, which is parametric w.r.t. different abstract domains. While the analyzer on the producer side typically has to compute a semantic fixpoint in a complex, iterative process, on the receiver it is only necessary to check that the certifícate is indeed a fixpoint of the abstract semantics equations representing the program. This is done in a single pass in a much more efficient process. ACC addresses the fundamental issues in PCC and opens the door to the applicability of the large body of frameworks and domains based on abstract interpretation as enabling technology for PCC. We present an overview of ACC and we describe in a tutorial fashion an application to the problem of resource-aware security in mobile code. Essentially the information computed by a cost analyzer is used to genérate cost certificates which attest a safe and efficient use of a mobile code. A receiving side can then reject code which brings cost certificates (which it cannot validate or) which have too large cost requirements in terms of computing resources (in time and/or space) and accept mobile code which meets the established requirements.

Estudio y mejora de un microinterruptor e implementación de un método de detección de islanding pasivo (IDM) basado en la monitorización de armónicos

Las microrredes son agrupaciones de fuentes de generación distribuida, cargas y elementos almacenadores de energía, que pueden actuar individualmente o conectadas a una red mayor. Debido a que presentan una serie de ventajas se están implantando de forma progresiva y creciente en los sistemas eléctricos de potencia. Son sistemas totalmente autónomos y, por ello, altamente flexibles. Ante una situación anómala que pueda producirse en la red principal, ya sea un fallo eléctrico, una disrupción física en la topología o una subida desproporcionada de precio, la microrred debe ser capaz de detectar esa situación y desconectarse a fin de poder protegerse. La situación de islanding se produce cuando por cualquier circunstancia hay una pérdida de la red principal y la microrred queda operando de forma aislada. Los métodos anti-islanding, que ayudan a la detección del fenómeno en las microrredes y a la desconexión de las mismas presentan dificultades a la hora de realizar esa tarea en determinados puntos del plano P-Q. Con este trabajo fin de Máster se pretende profundizar en el conocimiento y aplicabilidad de los métodos de detección de islanding extendidos a microrredes. Se analiza la viabilidad del microinterrumptor inteligente diseñado por los investigadores de la Universidad de Wisconsin - Madison para desarrollar la función de detección y actuación ante una situación de islanding inintencionado. A continuación se realiza un estudio de armónicos en el punto de conexión entre la red principal y la microrred. Por último se utilizan los resultados de este análisis para implementar y validar un nuevo método pasivo de detección de islanding en el microinterruptor basado en la medida y monitorización del nivel de tensión de 5º armónico en el PCC.