arXiv subjects

Santiago Escobar

Publications and source records attributed to Santiago Escobar.

23 records · Page 2Linked to original sources

arXiv2015

Proceedings XIV Jornadas sobre Programación y Lenguajes

This volume contains a selection of the papers presented at the XIV Jornadas sobre Programación y Lenguajes (PROLE 2014), held at Cádiz, Spain, during September 17th-19th, 2014. Previous editions of the workshop were held in Madrid (2013), Almería (2012), A Coruña (2011), Valéncia (2010), San Sebastián (2009), Gijón (2008), Zaragoza (2007), Sitges (2006), Granada (2005), Málaga (2004), Alicante (2003), El Escorial (2002), and Almagro (2001). Programming languages provide a conceptual framework which is necessary for the development, analysis, optimization and understanding of programs and programming tasks. The aim of the PROLE series of conferences (PROLE stems from the spanish PROgramación y LEnguajes) is to serve as a meeting point for spanish research groups which develop their work in the area of programming and programming languages. The organization of this series of events aims at fostering the exchange of ideas, experiences and results among these groups. Promoting further collaboration is also one of the main goals of PROLE.

cs.PL↗

arXiv2012

Proceedings 10th International Workshop on Reduction Strategies in Rewriting and Programming

This volume contains a selection of the papers presented at the 10th International Workshop on Reduction Strategies in Rewriting and Programming (WRS'2011), held on 29 May 2011 in Novi Sad, Serbia. Previous editions of the workshop were held in Utrecht (2001), Copenhagen (2002), Valencia (2003), Aachen (2004), Nara (2005), Seattle (2006), Paris (2007), Hagenberg (2008), Brasilia (2009), and Edinburgh (2010); the last one as a joint workshop with the STRATEGIES workshop. The WRS 2011 workshop was part of the Federated Conference on Rewriting, Deduction, and Programming (RDP'1), which grouped together different events including the 22th International Conference on Rewriting Techniques and Applications (RTA'11) and the 10th International Conference on Typed Lambda Calculi and Applications (TLCA'11).

cs.LO↗

arXiv2011

State Space Reduction in the Maude-NRL Protocol Analyzer

The Maude-NRL Protocol Analyzer (Maude-NPA) is a tool and inference system for reasoning about the security of cryptographic protocols in which the cryptosystems satisfy different equational properties. It both extends and provides a formal framework for the original NRL Protocol Analyzer, which supported equational reasoning in a more limited way. Maude-NPA supports a wide variety of algebraic properties that includes many crypto-systems of interest such as, for example, one-time pads and Diffie-Hellman. Maude-NPA, like the original NPA, looks for attacks by searching backwards from an insecure attack state, and assumes an unbounded number of sessions. Because of the unbounded number of sessions and the support for different equational theories, it is necessary to develop ways of reducing the search space and avoiding infinite search paths. In order for the techniques to prove useful, they need not only to speed up the search, but should not violate completeness, so that failure to find attacks still guarantees security. In this paper we describe some state space reduction techniques that we have implemented in Maude-NPA. We also provide completeness proofs, and experimental evaluations of their effect on the performance of Maude-NPA.

cs.CR↗

arXiv2010

Abstract Certification of Global Non-Interference in Rewriting Logic

Non-interference is a semantic program property that assigns confidentiality levels to data objects and prevents illicit information flows from occurring from high to low security levels. In this paper, we present a novel security model for global non-interference which approximates non-interference as a safety property. We also propose a certification technique for global non-interference of complete Java classes based on rewriting logic, a very general logical and semantic framework that is efficiently implemented in the high-level programming language Maude. Starting from an existing Java semantics specification written in Maude, we develop an extended, information-flow Java semantics that allows us to correctly observe global non-interference policies. In order to achieve a finite state transition system, we develop an abstract Java semantics that we use for secure and effective non-interference Java analysis. The analysis produces certificates that are independently checkable and are small enough to be used in practice.

cs.CR↗

arXiv2006

Removing Redundant Arguments Automatically

The application of automatic transformation processes during the formal development and optimization of programs can introduce encumbrances in the generated code that programmers usually (or presumably) do not write. An example is the introduction of redundant arguments in the functions defined in the program. Redundancy of a parameter means that replacing it by any expression does not change the result. In this work, we provide methods for the analysis and elimination of redundant arguments in term rewriting systems as a model for the programs that can be written in more sophisticated languages. On the basis of the uselessness of redundant arguments, we also propose an erasure procedure which may avoid wasteful computations while still preserving the semantics (under ascertained conditions). A prototype implementation of these methods has been undertaken, which demonstrates the practicality of our approach.

cs.PL↗