Automatic verification and certification of security and trust properties in communications protocols and mobile code

Abstract

Software products often lack an industrial guarantee of good performance, unlike the usual hardware products in IT. This fact, assumed by most users, is totally unacceptable in critical application domains, where explicit safety and security properties are established. Security properties are understood as those where the system is protected from the environment, e.g. attacks and security breaches, and safety properties are understood as those where the system environment is protected, e.g. accidental information leakage, mismanagement of shared resources, etc. We have developed techniques for the analysis, verification and certification of concurrent and/or reactive systems, i.e. systems with indeterministic and/or infinite behavior, and techniques for software systems in general, i.e. systems (possibly deterministic or finite) where actions taken over time may not be relevant, unlike concurrent systems, but certain properties satisfied at all times (invariant) or satisfied at some specific point in their execution (functional properties). In particular, we offer tools for: the analysis and verification of security properties in cryptographic communication protocols (e.g., Diffie-Hellman); the verification and certification of safety properties in mobile code (e.g., Java) and the verification of properties in generic software systems (e.g., mismanagement of shared resources).

Scientific officer

Escobar Román, Santiago

Stakeholders

Applications

  • Verification of cryptographic protocols.
  • Analysis of non-filtering and declassification of secret information.

Technical advantages

  • Verificación de propiedades de seguridad en protocolos de comunicaciones y verificación de propiedades de comportamiento en programas Java. Si el protocolo o aplicación no cumple las propiedades proporcionamos un contra ejemplo, para que dicho protocolo o aplicación pueda ser reparado.

Benefits it provides

  • We have developed the only technique on the market applied to the entire Java language.
  • Other techniques use toy programming languages while we analyze Java 1.4.

Relevant experience

The ELP group, created in 1989, is identified in the registry of consolidated research groups of the Generalitat Valenciana since October 2000 (key GR-00143). The group’s activity has been mainly related to multi-paradigm programming languages and rigorous methods for software development, focusing on rule-based programming and the use of abstract interpretation techniques and transformation techniques for the optimization of program execution. Rule-based languages have also been the basis for inductive programming and for the representation of complex but understandable models resulting from the extraction of knowledge from data (data mining). The ELP group has participated in more than 30 competitive projects financed with European, national and community funds. Its research activity has often been developed in connection with related groups based in foreign universities, including Germany (RWTH Aachen, U. of Kiel), Australia (Monash U.), Austria (Technische Universitat Wien), United States (U. of Illinois at Urbana-Champaign, National Research Laboratory, Portland State U., Washington, Stanford), France (- U. of Illinois at Urbana-Champaign, National Research Laboratory, Portland State U., Stanford University), France (- U. of Illinois at Urbana-Champaign, National Research Laboratory, Portland State U, Washington, Stanford), France (-‘Ecole Polytechnique, U. Grenoble, U. Nice, U. de Paris Sud), Italy (U. di Pisa, U. di Siena, U. di Udine) and United Kingdom (U. Bristol). The group has participated in several projects with companies where the group’s knowledge has been transferred or specific technology has been developed. The range of sectors in which the group has worked includes, logically, IT and consulting companies, but also companies ranging from distribution to hospital management. // The group ELP, created in 1989, was recognized as a consolidated group of the Valencian Government in October 2000 (reference GR-00143). The group’s activities have mainly focused on multi-paradigm programming languages and rigurous methods for software development, with particular focus on rule–based programming, and the use of abstract interpretation and program transformation techniques for the optimization of program execution. Rule-based languages have been also used for inductive programming and complex model representation that are also comprehensible as a result of knowledge discovering (data mining). The ELP group has participated in more than 30 competitive research projects funded by the EU, the Spanish Research Funding Agency, and other European foundations. The group keeps a good record of international collaborations. Including Germany (RWTH Aachen, U. Kiel), Australia (Monash U.), Austria (Technische Universit-“at Wien), USA (U. of Illinois at Urbana-Champaign, National Research Laboratory, Portland State U., Washington, Stanford), France (-‘Ecole Polytechnique, U. Grenoble, U. Nice, U. Paris Sud), Italy (U. di Pisa, U. di Siena, U. di Udine) and UK (U. Bristol). The Group also keeps a good record of collaboration with industry, including IT companies as well as hospital management and distribution companies.