2nd Prometidos-CM Winter School

16-17 December 2013

IMDEA Software Institute
Edificio IMDEA Software
Campus Montegancedo
28223-Pozuelo de Alarcón, Madrid
SPAIN

  1. About
  2. Registration
  3. Structure of the School
  4. List of Speakers / Talks
  5. Talks abstracts
    1. Álvaro Fernandez Diaz - Rigorous software development of Multi-Agent …
    2. François Dupressoir - Certified computer-aided cryptography: Efficient …
    3. Ignacio Fábregas - Coalgebraic and Categorical Techniques for the Study of …
    4. Dario Fiore - Verifiable Delegation of Computation on Outsourced Data
    5. Elena Gómez-Martínez / Ricardo J. Rodríguez - Modelling and Analysis of …
    6. Samir Genaim - Proving Program Termination
    7. César Kunz - Formal quantification of the probability of events
    8. Pablo Nogueira - Data Structures in Java
    9. Fernando Rosa Velardo - Enriched Petri nets for the verification of …
    10. Adrián Riesco - Generating test-cases by using narrowing in Maude
    11. Ismael Rodriguez Laguna - A General Testability Theory: Classes, …
    12. Benedikt Schmidt - Attacks and Proofs for Channel Establishment and Key …
  6. Program
  7. Location

About

PROMETIDOS-CM (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 (IMDEA-Software, CLIP-UPM, BABEL-UPM, FADOSS-UCM, GPD-UCM).

The scientific interests of PROMETIDOS-CM cover all aspects of development of software based on modular, scalable and realistic rigorous methods.

One of the strategic purposes of PROMETIDOS-CM is the realization of effective training actions to introduce young post-graduate 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 on-line registration. You only need to send a message to the organizers:

Pierre-Yves 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 PROMETIDOS-CM 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 Multi-Agent Systems
  • François Dupressoir - Certified computer-aided cryptography: Efficient provably secure machine code from high-level 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 test-cases by using narrowing in Maude
  • Elena Gómez-Martínez / Ricardo J. Rodríguez - Modelling and Analysis of Non-Functional Properties in Critical Systems with Petri Nets
  • Fernando Rosa Velardo - Enriched Petri nets for the verification of infinite-state systems
  • Benedikt Schmidt - Attacks and Proofs for Channel Establishment and Key Exchange Protocols

Talks abstracts

Álvaro Fernandez Diaz - Rigorous software development of Multi-Agent Systems

Slides

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 agent-oriented programming languages. However, there exist several formalisations available for programming languages that comply with the Belief-Desire-Intention Software Architecture (BDI).

In this talk, I will briefly introduce the agent-oriented 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 computer-aided cryptography: Efficient provably secure machine code from high-level implementations

Slides

We present a computer-aided framework for proving concrete security bounds for cryptographic machine code implementations. The front-end of the framework is an interactive verification tool that extends the EasyCrypt framework to reason about relational properties of C-like programs extended with idealised probabilistic operations, in the style of code-based 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 high-level, and is also instrumented to detect when compilation may interfere with side-channel countermeasures deployed in source code. We demonstrate the applicability of the framework with the RSA-OAEP 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 computer-aided cryptographic tools to real-world security, and the first application of CompCert to cryptographic software.

Ignacio Fábregas - Coalgebraic and Categorical Techniques for the Study of Process Semantics

Slides

To reason about computational systems it is customary to mathematically formalize them by means of state-based 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

Slides

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 input-size -- 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ómez-Martínez / Ricardo J. Rodríguez - Modelling and Analysis of Non-Functional Properties in Critical Systems with Petri Nets

Slides

A critical system must fulfill its mission despite the presence of harmful issues. Security, as a non-functional 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 non-functional 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 non-functional properties in a new system before deployment. Mainly, we focus in performance and security as properties of interest.

Samir Genaim - Proving Program Termination

Slides

The classic approach for proving program termination is to seek a ranking function that maps the program states to the elements of a well-founded order, such that it decreases when applied to consecutive states. This implies termination since infinite descent on well-founded 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

Slides

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 computer-aided 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 infinite-state systems

Slides

Petri nets are one of the most well-known models for distributed and concurrent infinite-state systems. They can be used to model dynamic networks of finite-state 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 Well-Structured Transition Systems, as well as a strict comparison of the different formalisms using their so-called coverability languages.

Adrián Riesco - Generating test-cases by using narrowing in Maude

Slides

Testing is one of the most important and most time-consuming 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

Slides

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

Slides

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:00-10:00 A. Riesco Generating test-cases by using narrowing in Maude
break --
10:15-11:15 F. R. Velardo Enriched Petri nets for the verification of infinite-state systems
break --
11:30-12:30 P. Nogueira Data Structures in Java
lunch --
14:00-15:00 Á. F. Diaz Rigorous software development of Multi-Agent Systems
break --
15:15-16:15 E. Gómez-Martínez Modelling and Analysis of Non-Functional Properties in Critical Systems with Petri Nets
15:15-16:15 R. J. Rodríguez Modelling and Analysis of Non-Functional Properties in Critical Systems with Petri Nets
break --
16:45-17:45 D. Fiore Verifiable Delegation of Computation on Outsourced Data

17th December 2013

Speaker Title
09:00-10:00 I. Fábregas Coalgebraic and Categorical Techniques for the Study of Process Semantics
break --
10:15-11:15 S. Genaim Proving Program Termination
break --
11:30-12:30 I. R. Laguna A General Testability Theory: Classes, properties, complexity, and testing reductions
lunch --
14:00-15:00 B. Schmidt Attacks and Proofs for Channel Establishment and Key Exchange Protocols
break --
15:15-16:15 C. Kunz Formal quantification of the probability of events
break --
16:45-17:45 F. Dupressoir Efficient provably secure machine code from high-level 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.


View Larger Map

Attachments