Iniciativa IMDEA

Inicio > Eventos > Software Seminar Series (S3)

Software Seminar Series (S3)

Niki Vazou

Tuesday, November 05, 2019

10:45am Meeting room 302 (Mountain View), level 3

Niki Vazou, Assistant Research Professor, Instituto IMDEA Software

Refinement Types 101

Abstract:

In this talk I will briefly explain how refinement types can are used for program verification. Refinement types use the modularity of types to reduce program verification into SMT decidable queries. The talk relies on a PLMW@ICFP 30 minutes presentation, so there will be plenty of time for Q&A.


Time and place:
10:45am Meeting room 302 (Mountain View), level 3
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Fernando Macías

Tuesday, October 29, 2019

10:45am Meeting room 302 (Mountain View), level 3

Fernando Macías, Post-doctoral Researcher, Instituto IMDEA Software

Multilevel Modelling and Domain-Specific Languages

Abstract:

Modern software engineering deals with demanding problems that yield large and complex software. The area of Model-Driven Software Engineering tackles this issue by using models during the development process, but it does not address some of the communication problems among different stakeholders. Domain-Specific Modelling Languages (DSML) aim at involving domain experts with non-technical profiles in that process. DSMLs define concepts with different levels of abstraction, but traditional modelling does not allow enough flexibility to organise them adequately. Multilevel Modelling (MLM) approaches provide an unbounded number of levels of abstraction, plus other features that perfectly fit DSMLs. Their development can also benefit from Model Transformations (MT), especially when these encode the behaviour of DSMLs. MTs can be exploited by MLM, becoming a precise and reusable definition of behaviour. In this talk, I outline the work that I presented in my PhD thesis, consisting of a MLM and Multilevel MT approach which tackles open issues in the field and compares it with the state of the art through literature review and experiments, providing its formalisation and its implementation in the tool MultEcore, together with case studies.


Time and place:
10:45am Meeting room 302 (Mountain View), level 3
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Anaïs Querol

Tuesday, October 22, 2019

10:45am Meeting room 302 (Mountain View), level 3

Anaïs Querol, PhD Student, Instituto IMDEA Software

STARKs in an eggshell

Abstract:

The general idea of STARKs is to transform a claim on a certain computation to another claim on the low-degreeness of one polynomial. This construction has gained a lot of attention during the past year, leading to several implementations in the wild. During this talk, we will explain how to build a STARK using genSTARK, one of these libraries. We will also share its complexity analysis based on the different parameters involved in Pedersen commitments computation, assuming very little mathematical background. Only some basic cooking notions will be expected from the audience. I will do a 30min rehearsal for my talk at the ZKProof Community Event in Amsterdam on October 29. This is a presentation of the summer internship I did at QEDIT, Tel Aviv.


Time and place:
10:45am Meeting room 302 (Mountain View), level 3
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Dimitris Kolonelos

Tuesday, October 08, 2019

10:45am Meeting room 302 (Mountain View), level 3

Dimitris Kolonelos, PhD Student, Instituto IMDEA Software

Zero-Knowledge Proofs for Set Membership: Efficient, Succinct, Modular

Abstract:

We consider the problem of proving in zero knowledge that an element of a public set satisfies a given property without disclosing the element, i.e. that for some u, “u ∈ S and P(u) holds”. This problem arises in many applications (anonymous cryptocurrencies, credentials or whitelists) where, for privacy or anonymity reasons, it is crucial to hide certain data while ensuring properties of such data. We design new modular and efficient constructions for this problem through new commit-and- prove zero-knowledge systems for set membership, i.e. schemes proving u ∈ S for a value u that is in a public commitment c_u . Being commit-and-prove, our solutions can act as plug-and-play modules in statements of the form “u ∈ S and P(u) holds” (by combining our set membership system with any other commit-and-prove scheme for P(u)). Also, they work with Pedersen commitments over prime order groups which makes them compatible with popular systems such as Bulletproofs or Groth16. Both public parameters and proofs in our solutions have constant-size (i.e., independent of the size of the sets). Compared to previous work that achieves similar properties—Camenisch and Lysyanskaya (CRYPTO 2002) and the clever techniques combining zkSNARKs and Merkle Trees in Zcash—our protocols offer more flexibility and 4× faster proving time for a set of size 2^60.


Time and place:
10:45am Meeting room 302 (Mountain View), level 3
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Luis Miguel Danielsson

Tuesday, September 24, 2019

10:45am Meeting room 302 (Mountain View), level 3

Luis Miguel Danielsson, PhD Student, Instituto IMDEA Software

Decentralized Stream Runtime Verification

Abstract:

We study the problem of decentralized monitoring of stream runtime verification specifications. Decentralized monitoring uses distributed monitors that communicate via a synchronous network, a communication setting common in many cyber-physical systems like automotive CPSs. Previous approaches to decentralized monitoring were restricted to logics like LTL logics that provide Boolean verdicts. We solve here the decentralized monitoring problem for the more general setting of stream runtime verification. Additionally, our solution handles network topologies while previous decentralized monitoring works assumed that every pair of nodes can communicate directly. We also introduce a novel property on specifications, called decentralized efficient monitorability, that guarantees that the online monitoring can be performed with bounded resources. Finally, we report the results of an empirical evaluation of an implementation and compare the expressive power and efficiency against state-of-the-art decentralized monitoring tools like Themis.


Time and place:
10:45am Meeting room 302 (Mountain View), level 3
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Manuel Bravo

Tuesday, September 17, 2019

10:45am Meeting room 302 (Mountain View), level 3

Manuel Bravo, Post-doctoral Researcher, Instituto IMDEA Software

Reconfigurable Atomic Transaction Commit

Abstract:

Modern data stores achieve scalability by partitioning data into shards and fault-tolerance by replicating each shard across several servers. A key component of such systems is a Transaction Certification Service (TCS), which atomically commits a transaction spanning multiple shards. Existing TCS protocols require 2f+1 crash-stop replicas per shard to tolerate f failures. In this work we present atomic commit protocols that require only f+1 replicas and reconfigure the system upon failures using an external reconfiguration service. We furthermore rigorously prove that these protocols correctly implement a recently proposed TCS specification. We present protocols in two different models--the standard asynchronous message-passing model and a model with Remote Direct Memory Access (RDMA), which allows a machine to access the memory of another machine over the network without involving the latter's CPU. Our protocols are inspired by a recent FARM system for RDMA-based transaction processing. Our work codifies the core ideas of FARM as distributed TCS protocols, rigorously proves them correct and highlights the trade-offs required by the use of RDMA.


Time and place:
10:45am Meeting room 302 (Mountain View), level 3
IMDEA Software Institute, Campus de Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Software Seminar Series (S3) - Primavera 2019