2nd PrometidosCM Winter School
1617 December 2013
IMDEA Software Institute
Edificio IMDEA Software
Campus Montegancedo
28223Pozuelo de Alarcón, Madrid
SPAIN
 About
 Registration
 Structure of the School
 List of Speakers / Talks

Talks abstracts
 Álvaro Fernandez Diaz  Rigorous software development of MultiAgent …
 François Dupressoir  Certified computeraided cryptography: Efficient …
 Ignacio Fábregas  Coalgebraic and Categorical Techniques for the Study of …
 Dario Fiore  Verifiable Delegation of Computation on Outsourced Data
 Elena GómezMartínez / Ricardo J. Rodríguez  Modelling and Analysis of …
 Samir Genaim  Proving Program Termination
 César Kunz  Formal quantification of the probability of events
 Pablo Nogueira  Data Structures in Java
 Fernando Rosa Velardo  Enriched Petri nets for the verification of …
 Adrián Riesco  Generating testcases by using narrowing in Maude
 Ismael Rodriguez Laguna  A General Testability Theory: Classes, …
 Benedikt Schmidt  Attacks and Proofs for Channel Establishment and Key …
 Program
 Location
About
PROMETIDOSCM (Madrid Program in Rigorous Methods for the Development of Software) is a R+D program funded by the regional government of Madrid, Spain, that involves some leading research groups in Computer Science in the region (IMDEASoftware, CLIPUPM, BABELUPM, FADOSSUCM, GPDUCM).
The scientific interests of PROMETIDOSCM cover all aspects of development of software based on modular, scalable and realistic rigorous methods.
One of the strategic purposes of PROMETIDOSCM is the realization of effective training actions to introduce young postgraduate and PhD students in the research area of rigorous methods. The announced Winter School attempts to be a contribution in this sense.
Registration
This Winter School is organized in a quite lightweight way. There are neither attendance fees nor a formal online registration. You only need to send a message to the organizers:
PierreYves Strub (pierreyves.strub [at] imdea.org)
A certificate of assistance will be given at the end of the School.
Structure of the School
The Second PROMETIDOSCM Winter School will consist of a series of talks given by experienced researchers affiliated to the program partners.
The talks are intended to be both attractive and rigorous. Some of them will include practical demonstrations.
List of Speakers / Talks
 Álvaro Fernandez Diaz  Rigorous software development of MultiAgent Systems
 François Dupressoir  Certified computeraided cryptography: Efficient provably secure machine code from highlevel implementations
 Ignacio Fábregas  Coalgebraic and Categorical Techniques for the Study of Process Semantics
 Dario Fiore  Verifiable Delegation of Computation on Outsourced Data
 Samir Genaim  Proving Program Termination
 César Kunz  Formal quantification of the probability of events
 Ismael Rodriguez Laguna  A General Testability Theory: Classes, properties, complexity, and testing reductions
 Pablo Nogueira  Data Structures in Java
 Adrián Riesco  Generating testcases by using narrowing in Maude
 Elena GómezMartínez / Ricardo J. Rodríguez  Modelling and Analysis of NonFunctional Properties in Critical Systems with Petri Nets
 Fernando Rosa Velardo  Enriched Petri nets for the verification of infinitestate systems
 Benedikt Schmidt  Attacks and Proofs for Channel Establishment and Key Exchange Protocols
Talks abstracts
Álvaro Fernandez Diaz  Rigorous software development of MultiAgent Systems
In order to implement a software system, there exists a relatively wide variety of successful (i.e. extensively utilised) programming languages available. However, a formalisation of their program semantics is not always available. This lack of formal semantics hinders (if not absolutely prevents) the application of formal verification techniques, like model checking or theorem proving, to the software systems implemented.
This situation is especially recurrent in the case of agentoriented programming languages. However, there exist several formalisations available for programming languages that comply with the BeliefDesireIntention Software Architecture (BDI).
In this talk, I will briefly introduce the agentoriented programming paradigm. Concretely, those following the BDI. Then I will describe different works aimed at the provision of formal semantics to the AGENTSPEAK programming language and its evolution into its interpreters Jason and eJason (the latter one being currently developed at UPM). I will emphasise why having only an informal semantics does not suffice.
François Dupressoir  Certified computeraided cryptography: Efficient provably secure machine code from highlevel implementations
We present a computeraided framework for proving concrete security bounds for cryptographic machine code implementations. The frontend of the framework is an interactive verification tool that extends the EasyCrypt framework to reason about relational properties of Clike programs extended with idealised probabilistic operations, in the style of codebased security proofs. The framework also incorporates an extension of the CompCert certified compiler to support trusted libraries, providing complex arithmetic calculations, or instantiating idealised components such as sampling operations. This certified compiler allows us to carry to executable code the security guarantees established at the highlevel, and is also instrumented to detect when compilation may interfere with sidechannel countermeasures deployed in source code. We demonstrate the applicability of the framework with the RSAOAEP encryption scheme, as standardized in PKCS!#1 v2.1. The outcome is a rigorous analysis of the advantage of an adversary to break the security of assembly implementations of the algorithms specified by the standard. The example also provides two contributions of independent interest: it is the first application of computeraided cryptographic tools to realworld security, and the first application of CompCert to cryptographic software.
Ignacio Fábregas  Coalgebraic and Categorical Techniques for the Study of Process Semantics
To reason about computational systems it is customary to mathematically formalize them by means of statebased structures such as labeled transitions systems, modal transition systems, or Kripke structures. The range of structures used to formalize computational systems is quite wide. In this context, coalgebras have emerged with a unifying aim. We will show a categorical study of process semantics with a particular emphasis on the study of the relationships between these, that is, a study of bisimulation and simulation relations, mainly Hughes and Jacobs notion of categorical (bi)simulation. We will translate to the coalgebraic setting some results already established for simulations in process algebra. Those are reflection and preservation of logical properties and to look for some unifying coalgebraic presentation of the standard simulations in process algebra. This work also led us to the definition of two new simulations that try to capture the fact that it is not always the case that "the larger the number of behaviors, the better'".
Dario Fiore  Verifiable Delegation of Computation on Outsourced Data
We address the problem in which a client stores a large amount of data with an untrusted server in such a way that, at any moment, the client can ask the server to compute a function on some portion of its outsourced data. In this scenario, the client must be able to efficiently verify the correctness of the result despite no longer knowing the inputs of the delegated computation, it must be able to keep adding elements to its remote storage, and it does not have to fix in advance (i.e., at data outsourcing time) the functions that it will delegate. Even more ambitiously, clients should be able to verify in time independent of the inputsize  a very appealing property for computations over huge amounts of data.
In this talk I will present novel cryptographic techniques that solve the above problem for the class of computations which can be expressed by arithmetic circuits of bounded degree. In particular I will discuss an efficient solution for the case of quadratic polynomials over a large number of variables. This class covers a wide range of significant arithmetic computations  notably, many important statistics. To confirm the efficiency of our solution, we show encouraging performance results, e.g., correctness proofs have size below 1 kB and are verifiable by clients in less than 10 milliseconds.
Elena GómezMartínez / Ricardo J. Rodríguez  Modelling and Analysis of NonFunctional Properties in Critical Systems with Petri Nets
A critical system must fulfill its mission despite the presence of harmful issues. Security, as a nonfunctional system property, needs to be conceived as an integral part of the development system process and as a singular need of what the system should perform. Thus, when designing critical systems it is fundamental to study the security issues that may occur and plan how to react to them, in order to keep fulfilling the system functional and nonfunctional requirements.
However, the addition of security to a system has not free cost. In fact, security costs can be very relevant and may span along different dimensions, such as budgeting, performance and reliability.
In this talk, we introduce the Petri nets formalism and show how it can help to evaluate nonfunctional properties in a new system before deployment. Mainly, we focus in performance and security as properties of interest.
Samir Genaim  Proving Program Termination
The classic approach for proving program termination is to seek a ranking function that maps the program states to the elements of a wellfounded order, such that it decreases when applied to consecutive states. This implies termination since infinite descent on wellfounded orders is impossible.
Different approaches differ in the kind of functions they search, and in the underlying techniques they use for this search. In this lecture I will overview techniques for seeking linear and lexicographic linear ranking function. In particular techniques that reduce the problem of synthesizing such a function to solving corresponding linear programming problems.
César Kunz  Formal quantification of the probability of events
In this talk, I will present a program logic for probabilistic programs, allowing one to prove upper, lower, or exact bounds for the probability of events, and to reason about program termination. This logic can also be used to reason about program equivalence. The support for this probabilistic Hoare logic is a recent addition to EasyCrypt?, a computeraided framework for building and verifying cryptographic proofs. It supplants (automated) heuristics from earlier versions of EasyCrypt?, that were restricted to prove upper bounds on the probability of events (in particular, they could not reason about probability of termination), and were too weak and impractical for many examples.
Pablo Nogueira  Data Structures in Java
We shall implement a few interesting data structures using the popular Java programming language and explain the advantages and disadvantages of Java particulars regarding interfaces, inheritance, generics, and polymorphic variables. A basic knowledge of Java is desirable, but I will adapt the contents of the seminar to the audience.
Fernando Rosa Velardo  Enriched Petri nets for the verification of infinitestate systems
Petri nets are one of the most wellknown models for distributed and concurrent infinitestate systems. They can be used to model dynamic networks of finitestate processes or communication through unbounded unordered buffers. However, some features like process identifiers or ordered communication cannot be modelled by classic Petri nets. In this lecture I will survey some extensions of the classical formalism, sometimes uniformly called Enriched Petri nets, that push further their expressiveness limits, while maintaining good decidability properties for their verification. I will present these properties under the common framework of WellStructured Transition Systems, as well as a strict comparison of the different formalisms using their socalled coverability languages.
Adrián Riesco  Generating testcases by using narrowing in Maude
Testing is one of the most important and most timeconsuming tasks in the software developing process, and thus techniques and systems to automatically generate and check test cases have become crucial. In this talk we show how to use the new narrowing commands available in Maude to test Maude specifications. Moreover, and given that Maude is a logical framework where other logics can be specified, we show how to generate test cases for programs written on languages previously defined in Maude.
Ismael Rodriguez Laguna  A General Testability Theory: Classes, properties, complexity, and testing reductions
We present a general framework to reason about testing. The difficulty of testing is assessed in terms of the amount of tests that must be applied to determine whether the system is correct or not. Based on this criterion, five testability classes are presented and related. These classes denote, respectively, the following five cases: (a) there exists a finite complete test suite; (b) any partial distinguishing rate can be reached with some finite test suite; (c) there exists a countable complete test suite; (d) there exists a complete test suite; and (e) all cases.
We also explore conditions that enable and disable finite testability, and their relation to testing hypotheses is studied. We measure how far incomplete test suites are from being complete, which allows us to compare and select better incomplete test suites. The complexity of finding minimum complete test suites is identified.
Furthermore, we address the reduction of testing problems to each other, that is, we study how the problem of finding test suites to test systems of some kind can be reduced to the problem of finding test suites for another kind of systems. This enables to export testing methods.
In order to illustrate how general notions are applied to specific cases, many typical examples from the formal testing techniques domain are presented.
Benedikt Schmidt  Attacks and Proofs for Channel Establishment and Key Exchange Protocols
Secure channels are an important building block for modern communication infrastructures. In this talk, I will first give an overview of the Transport Layer Security (TLS) protocol and its desired security properties, also sketching some of the recent attacks. I will then focus on key exchange protocols and their adversary models. Key exchange protocols are often combined with symmetric encryption to obtain secure channel protocols. In the last part of the talk, I will present the Tamarin tool which we will use to perform automated analysis of key exchange protocols in the symbolic model.
Program
16th December 2013
Speaker  Title  
09:0010:00  A. Riesco  Generating testcases by using narrowing in Maude 
break    
10:1511:15  F. R. Velardo  Enriched Petri nets for the verification of infinitestate systems 
break    
11:3012:30  P. Nogueira  Data Structures in Java 
lunch    
14:0015:00  Á. F. Diaz  Rigorous software development of MultiAgent Systems 
break    
15:1516:15  E. GómezMartínez  Modelling and Analysis of NonFunctional Properties in Critical Systems with Petri Nets 
15:1516:15  R. J. Rodríguez  Modelling and Analysis of NonFunctional Properties in Critical Systems with Petri Nets 
break    
16:4517:45  D. Fiore  Verifiable Delegation of Computation on Outsourced Data 
17th December 2013
Speaker  Title  
09:0010:00  I. Fábregas  Coalgebraic and Categorical Techniques for the Study of Process Semantics 
break    
10:1511:15  S. Genaim  Proving Program Termination 
break    
11:3012:30  I. R. Laguna  A General Testability Theory: Classes, properties, complexity, and testing reductions 
lunch    
14:0015:00  B. Schmidt  Attacks and Proofs for Channel Establishment and Key Exchange Protocols 
break    
15:1516:15  C. Kunz  Formal quantification of the probability of events 
break    
16:4517:45  F. Dupressoir  Efficient provably secure machine code from highlevel implementations 
Location
The School will be held at the IMDEA Software Institute building.
Please, have a look at the following page to get detailed direction instructions.
Attachments

generatingtestcasesbyusingnarrowing.pdf
(292.7 kB)  added by pierre
5 years ago.
Generating testcases by using narrowing

EnrichedPetrinetsfortheverificationofinfinitestatesystems.pdf
(0.9 MB)  added by pierre
5 years ago.
Enriched Petri nets for the verification of infinitestate systems
 RigorousSoftwareDevelopmentofMultiAgentSystems (2 bytes)  added by pierre 5 years ago.

RigorousSoftwareDevelopmentofMultiAgentSystems.pdf
(1.4 MB)  added by pierre
5 years ago.
RigorousSoftwareDevelopmentofMultiAgentSystems RigorousSoftwareDevelopmentofMultiAgentSystems

ModellingandAnalysisofNonFunctionalPropertiesinCriticalSystemswithPetriNets.pdf
(1.6 MB)  added by pierre
5 years ago.
ModellingandAnalysisofNonFunctionalPropertiesinCriticalSystemswithPetriNets

ModellingandAnalysisofNonFunctionalPropertiesinCriticalSystemswithPetriNets.2.pdf
(1.8 MB)  added by pierre
5 years ago.
ModellingandAnalysisofNonFunctionalPropertiesinCriticalSystemswithPetriNets

Formalquantificationoftheprobabilityofevents.pdf
(448.9 kB)  added by pierre
5 years ago.
Formal quantification of the probability of events

Ageneraltestabilitytheory.pdf
(1.2 MB)  added by pierre
5 years ago.
A General Testability Theory

CoalgebraicandCategoricalTechniquesfortheStudyofProcessSemantics.pdf
(0.8 MB)  added by pierre
5 years ago.
Coalgebraic and Categorical Techniques for the Study of Process Semantics

Provingprogramtermination.pdf
(11.2 MB)  added by pierre
5 years ago.
Proving Program Termination

Attacks_and_Proofs_for_Channel_Establishment_and_Key_Exchange_Protocols.pdf
(13.4 MB)  added by pierre
5 years ago.
Attacks and Proofs for Channel Establishment and Key Exchange Protocols

Certifiedcomputeraidedcryptography.pdf
(134.4 kB)  added by pierre
5 years ago.
Certified computeraided cryptography

EVHMACPrometidos.pdf
(5.3 MB)  added by pierre
5 years ago.
EVHMACPrometidos