The researcher from the IMDEA Software Institute,, Isabel García successfully presented her thesis last Wednesday, July 21. "A scalable static analysis framework for reliable program development exploiting incrementality and modularity" is the title of the work developed by the researcher, directed by the distinguished professor and former director of the Institute, Manuel Hermenegildo. With this thesis, Isabel completes her doctoral studies in artificial intelligence at the Polytechnic University of Madrid (UPM).
Her object of study comes in response of the trend pattern, automatic source code analysis and verification is of great importance both at the level of software development and software maintenance.
Automatic static analysis tools allow inferring properties about software without executing it and without the need for human interaction. When these tools are based on formal methods, the properties are guaranteed to hold and come with a mathematical proof. The usage of these tools during the coding, testing, and maintenance phases of the software development cycle helps reduce efforts in terms of time and cost, as they contribute to the early detection of bugs, automatic optimizations, or automatic documentation. The increasing importance of the reliability of evolving software is evidenced by the current number of tools and on-line platforms for continuous integration and deployment. In this setting, when changes happen fast, analysis tools are only useful if they are precise and, at the same time, scalable enough to provide results before the next change happens.
In this thesis she studies scalable analyses in the context of abstract interpretation. Since a way to improve scalability is to perform coarser abstractions, she first inspect what effect this may have in effectively proving the absence of bugs. Second, she presents a framework for scalable static analyses which is generic, that is, independent of the data abstraction of the program. Isabel presents several algorithms for incrementally reanalyzing whole programs in a context-sensitive manner, reusing as much as possible previous analysis results. A key novel aspect of the approach is to take advantage of the modular structure of programs, typically as defined by the programmer, while keeping a fine-grained relation between the analysis result and the source program.
Additionally, she presents a mechanism for the programmer to help the analyzer in terms of precision and performance by means of assertions. She shows that these assertions together with incremental analysis are specially useful when analyzing generic code. All these algorithms have been implemented and evaluated for different abstract domains within the CiaoPP framework.
Lastly, she presents an application of the analysis framework to perform on-the-fly assertion checking, providing continuous and almost instantaneous feedback to the programmer as the code is written. Her initial experience with this integrated tool shows quite promising results, with low latency times that provide early, continuous, and precise “on-the-fly” semantic feedback to programmers during the development process. This allows detecting many types of errors including swapped variables, property incompatibilities, illegal calls to library predicates, violated numeric constraints, unintended behavior w.r.t. termination, resource usage, determinism, covering and failure, etc.
Two PhD researchers of the IMDEA Software Institute, Anaïs Querol and Silvia Sebastián, have participated at the UPM contest "Your thesis in a nutshell" which consisted in uploading a video with a short and not technical explanation of their thesis.
Both of them, Silvia and Anaïs were selected between the top ten and received a recognition and 500 euros prize for it. This recognition entailed participating in person in a special award event and presenting their thesis live. Anaïs was also selected by the jury to receive the second prize.
We are proud that researchers from the institute participate in events like these and even more proud of their achievements.
Researchers from the research unit "Security and Privacy" at TU Wien (Lukas Aumayr and his supervisor Prof. Matteo Maffei) in collaboration with the IMDEA Software Institute (Prof. Pedro Moreno-Sánchez, previously postdoc at TU Wien) and the Purdue University (Prof. Aniket Kate) have jointly developed a protocol that makes more secure and faster transactions in cryptocurrencies like Bitcoin.
Nowadays in cities like Tokyo we can subsist with cryptocurrencies like Bitcoin. Buying a coffee, going shopping, taking the bus, paying a taxi drive or even a meal are all accessible if you only got Bitcoin in your (electronic) wallet. This may seem strange for some European countries, -even though there are many cryptocurrencies in the market like ATM and coinradar (Spanish market)- but we are walking at a steady speed to that model that may or may not co-exist with our bank cards in the future.
The popularity of cryptocurrencies is increasing very fast due to the many advantages compared to, for example, Mastercard or Visa. Transactions are usually anonymous, decentralized and global (i.e., same currency is accepted worldwide).
But there is still work to do in security, privacy and efficiency. Fraud can be possible, users can discover information about other users that should be kept secret, the number of transactions is limited, and sometimes delays occur.
The researchers from the IMDEA Software Institute, TU Wien, and Purdue University, aware of these problems, have developed an improved protocol. The article, in which these ideas are based on, will be presented at the [USENIX Security Symposium 2021], one of the best IT security conferences worldwide.
The bottleneck of Bitcoin
"It has long been known that Bitcoin and other blockchain technologies have a scalability problem: There can only be a maximum of ten transactions per second," says Lukas Aumayr of the Security and Privacy research unit at TU Wien. "That's very few compared to credit card companies, for example, which perform tens of thousands of transactions per second worldwide."
An approach to solve this problem is the "Lightning Network" - an additional network of payment channels between blockchain users. For example, if two people want to process many transactions in a short period of time, they can exchange payments directly between each other in this way, without each individual transaction being published on the blockchain. Only at the beginning and at the end of this series of transactions is there an official entry in the blockchain.
As demonstrated by other works of Pedro (IMDEA Software Institute), the apparent privacy gain of the Lightning Network due to off-chain payments isn’t real. In fact, previous work of Pedro has demonstrated that payment intermediaries can learn who pays what to whom. This is an issue that needs to be solved for a system like Lightning Network to become widely used.
A second big issue is that “in addition, everyone in this chain has to contribute a certain amount of money, which is locked as collateral. Sometimes a transaction fails, and then a lot of money can remain locked for a relatively long time – the more people involved, the longer time it will take” says Pedro Moreno-Sánchez.
Mathematically ruling out vulnerabilities
“This project has advanced the state of off-chain payments both theoretically and practically. From the theory point of view, we have provided a formal model of the new payment system, proving mathematically its correctness and security against an adversary. Moreover, while current Lightning Network requires two rounds of communication across all participants in a payment, Blitz (the new protocol) reduces it to a single round of communication. This is a milestone result since Lightning Network and other approaches proposed so far where all using two rounds and it was unknown whether we could beat this barrier” in the IMDEA Software researcher’s words.
“In practice, a single round of communication implies great benefits in practicality” As Lukas said: In the first round, the money is locked, in the second round it is released - or refunded if there were problems. That could mean an extra day of delay for each user in that chain. With our protocol, the communication chain only has to be run through once”
Simulation proves practicality
However, it is not only the fundamental logical structure of the new protocol that is important, but also its practicality. Therefore, the team simulated in a payment channel network how the new technology behaves compared to the previous Lightning network. The advantages of the new protocol became particularly apparent: depending on the situation, such as the number of attacks and fraud attempts, the new protocol results in a factor of 4 to 33 fewer failed transactions than with the conventional Lightning network.
Pedro and Lukas are putting efforts on disseminating the results with the Lightning Network developers as well as other Bitcoin organizations. One of the most attractive points so far is that Blitz is totally backwards compatible with currently deployed technologies and could be immediately deployed as a more secure and faster alternative for off-chain payments.
The researchers of the IMDEA Software Institute, César Sánchez and Felipe Gorostiaga together with Gerardo Schneider (University of Gothenburg), Sebastian Zudaire and Sebastian Uchitel (both from Universidad de Buenos Aires) have presented the paper: "Assumption Monitoring Using Runtime Verification for UAV Temporal Task Plan Executions" at IEEE International Conference on Robotics and Automation (ICRA 2021).
Temporal task planning guarantees a robot will succeed in its task as long as certain explicit and implicit assumptions about the robot’s operating environment, sensors, and capabilities hold. A robot executing a plan can silently fail to fulfill the task if the assumptions are violated at runtime. Monitoring assumption violations at runtime can flag silent failures and also provide mitigation and remediation opportunities. However, this requires means for describing assumptions combining temporal and quantitative data, automatic construction of correct monitors and ensuring a correct interplay between the planning execution and monitors.
"In this paper we propose combining temporal planning with stream runtime verification, which offers a high-level language to describe monitors together with guarantees on execution time and memory usage. We demonstrate our approach both in real and simulated flights for some typical mission scenarios."
IMDEA Software Institute researchers Marco Guarnieri and Pepe Vila together with Boris Köpf (Microsoft Research) and Jan Reineke (Saarland University) won a best paper award at the 42nd IEEE Symposium on Security and Privacy (S&P) for their paper “Hardware-Software Contracts for Secure Speculation”.
The paper develops a framework for defining hardware-software contracts that capture hardware side-channel security guarantees in a simple, mechanism-independent manner. The framework provides foundations for principled co-design of hardware and software for side-channel resistant systems. Using this framework, the authors characterize the security guarantees provided by recent hardware mechanisms for secure speculation; mapping each mechanism to a set of hardware-software contracts. Contracts are also the basis for secure programming, where different contracts impose distinct software-level requirements for end-to-end security.
The work was supported by a grant from Intel Corporation, Atracción de Talento Investigador grant 2018- T2/TIC-11732A, Juan de la Cierva-Formación grant FJC2018- 036513-I, Spanish project RTI2018-102043-B-I00 SCUM, and Madrid regional project S2018/TCS-4339 BLOQUES.
Data has emerged as the oil of the 21st century. The importance of data is no longer surprising, but its growing relevance is beginning to take on worrying overtones. Our lives are increasingly dependent on technology that seems to need our data. But where is our data? Where is it stored? Due to the ubiquity of the Internet, everything is now migrated to the cloud.
Zara, Spotify, Netflix, Twitter, practically all companies today use data on which they compute to give us a better service. For example, a music recommendation service should store what we have listened to and cross-reference that data with the data of other people with whom there is a match to try to deduce what else we might like. A financial service could do something similar with investment funds, which is arguably more sensitive information. The same could happen with health data, held by the public health provider or a private company. And all of them, moreover, often have personal information: addresses, email accounts, bank account numbers...
Almost all of these companies rely on external providers for their computing needs: storing data (i.e., delegating its storage) and using it to extract results by running programs on these providers' computers (delegating a computation).
How can we ensure that data and computations that are delegated to third parties are protected against espionage and run correctly? Data can be encrypted, but in order for it to be used by existing software, it needs to be decrypted. At that point, a malicious provider (or a provider that gets hacked) can inspect it and learn data that the company that stored it does not want to disclose and that the person to whom it refers probably does not want to disclose either. Similarly, it could change the program that executes the calculations and return incorrect results, which raises the question of how to check that such results are correct without redoing the computation?
Cryptographic techniques exist to solve both problems. Advancing on them and making them usable in practice is the main objective of the PICOCRYPT project (Cryptography for Privacy and Integrity of Computation on Untrusted Machines), proposed by Dr. Dario Fiore, a researcher at the IMDEA Software Institute of the Madrid Regional Government, which has recently been awarded a Consolidator ERC grant from the European Union (Horizon 2020 research and innovation programme*) to receive funding worth 2 million euros over five years. The European Research Council is the European Union's most prestigious scientific and funding programme. With PICOCRYPT, the IMDEA Software Institute has been granted three projects by this programme (together with RACCOON and MATHADOR).
For Dr. Dario Fiore, cryptography is already a key component to keep our data secure during communication, but "the challenge of PICOCRYPT is to invent new cryptographic protocols to keep our data secure also during computation. The benefits of this paradigm are innumerable. For example, there are people and companies who refrain from using external IT resources because of the risks of this model. With the solutions we intend to design in PICOCRYPT, they could instead use these services securely and without having to fully rely on the providers of these services". It will therefore guarantee the integrity and privacy of computation made with data stored in the cloud and also make it efficient to ensure that delegation is cost-effective.
The IMDEA Software Institute is one of the seven IMDEA Institutes promoted by the Regional Government of Madrid with the aim of carrying out research and scientific development at the highest level.
*“This project has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (Grant agreement No. 101001283)”
The 42nd IEEE Symposium on Security and Privacy have recently published the list of accepted papers for the conference that will take place from the 23rd to 27th of May. We are happy to announce that six papers from researchers of the IMDEA Software Institute are between them.
Since 1980, the IEEE Symposium on Security and Privacy has been the premier forum for presenting developments in computer security and electronic privacy, and for bringing together researchers and practitioners in the field. The 2021 Symposium will mark the 42nd annual meeting of this flagship conference, sponsored by the IEEE Computer Society Technical Committee on Security and Privacy in cooperation with the International Association for Cryptologic Research.
The following papers have been accepted:
A2L: Anonymous Atomic Locks for Scalability in Payment Channel Hubs
Erkan Tairi (TU Wien), Pedro Moreno-Sanchez (IMDEA Software Institute), Matteo Maffei (TU Wien).
Hardware-Software Contracts for Secure Speculation
Marco Guarnieri (IMDEA Software Institute), Boris Köpf (Microsoft Research), Jan Reineke (Saarland University), Pepe Vila (IMDEA Software Institute).
High-Assurance Cryptography in the Spectre Era
Gilles Barthe (Max Planck Institute for Security and Privacy and IMDEA Software Institute), Sunjay Cauligi (University of California San Diego), Benjamin Gregoire (INRIA Sophia Antipolis), Adrien Koutsos (Max Planck Institute for Security and Privacy), Kevin Liao (Max Planck Institute for Security and Privacy and Massachusetts Institute of Technology), Tiago Oliveira (University of Porto (FCUP) and INESC TEC), Swarn Priya (Purdue University), Tamara Rezk (INRIA Sophia Antipolis), Peter Schwabe (Max Planck Institute for Security and Privacy).
How Did That Get In My Phone? Unwanted App Distribution on Android Devices Stephan van Schaik (University of Michigan), Marina Minkin (University of Michigan), Andrew Kwong (University of Michigan), Daniel Genkin (University of Michigan), Yuval Yarom (University of Adelaide and Data61), Platon Kotzias (NortonLifelock Research Group), Juan Caballero (IMDEA Software Institute), Leyla Bilge (NortonLifelock Research Group).
SoK: Computer-Aided Cryptography
Manuel Barbosa (University of Porto and INESC TEC), Gilles Barthe (Max Planck Institute for Security and Privacy; IMDEA Software Institute), Karthik Bhargavan (INRIA Paris), Bruno Blanchet (INRIA Paris), Cas Cremers (CISPA Helmholtz Center for Information Security), Kevin Liao (Max Planck Institute for Security and Privacy; Massachusetts Institute of Technology), Bryan Parno (Carnegie Mellon University).
Bitcoin-Compatible Virtual Channels Lukas Aumayr (Technische Universität Wien), Oguzhan Ersoy (Delft University of Technology), Andreas Erwig (Technische Universität Darmstadt), Sebastian Faust (Technische Universität Darmstadt), Kristina Hostáková (ETH Zürich), Matteo Maffei (Technische Universität Wien), Pedro Moreno-Sanchez (Technische Universität Wien; IMDEA Software Institute), Siavash Riahi (Technische Universität Darmstadt).
The IMDEA Software Institute researcher Maximiliano Klemen has successfully defended his PhD thesis on: "A General Framework for Static Resource Analysis and Profiling of (Parallel) Programs and an Application to Runtime Checking", supervised by Prof. Pedro López, on March 5th.
The goal of static cost analysis is to automatically estimate the resources used by program executions without running the programs with concrete data, as functions of input data sizes and possibly other (environmental) parameters. In this thesis he improves and extends state-of-the-art static cost analysis techniques by developing a novel, general and flexible framework for resource usage analysis that can be easily instantiated to infer a wide range of resources, notions of costs, and approximations, which can deal with different programming languages, platforms and execution models.
For some applications, standard resource analyses, which estimate the total resource usage of a program, do not provide the information required. For example, helping developers make resource-related design decisions requires knowing how such total resource usage is distributed over selected parts of a program. The novel, general, and flexible framework developed in Maximiliano's thesis solves this problem, by allowing setting up cost relations that can be instantiated for performing a wide range of resource usage analyses, including both static profiling and the standard notion of cost. He shows how to instantiate such framework to perform static profiling of accumulated cost (also parameterized by input data sizes). Such information identifies the parts of the program that have the greatest impact on the total program cost.
Moreover, parallel computing has become the dominant paradigm in computer architecture, and predicting resource usage on such platforms poses a difficult challenge. We address it by extending and instantiating our general framework for performing resource usage analysis of parallel (logic) programs. Besides cost functions, the analysis also infers other useful information to better exploit and assess the potential and actual parallelism of a system. He also develops a novel application of his cost analysis framework: inferring static performance guarantees for programs with run-time checks. Instrumenting programs for performing run-time checking of properties, such as regular shapes, is a common and useful technique that helps programmers detect incorrect program behaviors. However, such run-time checks inevitably introduce run-time overhead (in execution time, memory, energy, etc.). He proposes a method that uses static analysis to estimate such overhead. This approach can provide guarantees for all possible execution traces, and allows assessing how the overhead grows as the size of the input, which is a parameter of the estimated cost functions, grows. His method also extends an existing assertion verification framework to express “admissible” overheads, and statically and automatically checks whetherthe instrumented program conforms with such specifications.
The accuracy and applicability of his framework strongly depend on the capabilities of the component in charge of solving (or safely approximating) the cost and size recurrence relations generated during the analysis. In this thesis he proposes techniques for solving recurrence relations that extend state-of-the-art solvers, addressing some of their limitations. In particular, he develops a novel approach for solving arbitrary, constrained recurrence relations. It is a guess and check approach that uses well-known machine learning techniques for the guess stage, and a combination of an SMT-solver and a Computer Algebra System for the check stage. Additionally, he develops a method for solving cost relations involving a maximization operator, which appears when representing complex size and cost relations.
Finally, he reports on the implementation of the techniques developed in this thesis within the CiaoPP system and their experimental evaluation, obtaining encouraging results.
The Association for Logic Programming (ALP) was founded in 1986, with the mission to contribute to the development of Logic Programming, relating it to other areas, and to promote its uses in academia and industry worldwide.
The ALP Board is the governing body of the association and is in charge of defining priorities, supervising the journal (TPLP), organizing conferences and Summer schools, etc., and in particular proposing General and Program Committee Chairs for the different conferences organized by the Association.
ALP Executive Board members are elected by a popular vote within the community among candidates proposed for their contributions and recognition within logic programming.
The researcher from thr Institute IMDEA Software, Alejandro Aguirre, advised by Prof. Gilles Barthe, has recently defended his thesis successfully: "Relational logics for higher-order effectful programs".
Relational logics are used to express what properties of two executions of the same program or two executions of two different programs have in common. Properties such as program equivalence, non-interference, differential privacy, robustness or sensitivity fall under this umbrella.
Although traditional program verification offers the capability to prove relational properties by using program transformation, ultimately these fall short because they are unable to use the program structure to guide the reasoning. On the other hand, novel logics explicitly designed for relational reasoning are often overly reliant on reasoning synchronously, that is, about programs with similar syntactic structure.
In this study, Alejandro starts by developing Relational Higher-Order Logic (RHOL), a logic to prove relational properties of a pair of pure functional programs that can reason synchronously when the programs have the same syntax, but also has a wide variety of one-sided rules that allows the reasoning to progress when the programs lack this similarity. RHOL also has a companion system, Unary Higher-Order Logic (UHOL) that can be used to prove unary properties (i.e., properties of a single program). Both RHOL and UHOL are based on a standard Higher-Order Logic (HOL). RHOL is not only a logic in its own right, but can also be seen as a framework in which to embed other relational reasoning systems to prove their soundness, as well as a base on top of which to build more expressive logics.
The author demonstrates the versatility of RHOL by using it to support different extensions with the aim of reasoning about probabilistic programs. He first focus on lifting-based properties. Liftings provide a way to erase the computational side effects from logical specifications, so that they can reason about them using standard logics. Some properties that can be proven in this manner are bounds on the probability that the program output satisfies a certain property, or differential privacy. He respectively embed reasoning about these two properties into two novel logics: Higher-Order Union Bound Logic (HO-UBL) and Higher-Order Relational Probabilistic Logic (HO-RPL). He then extends these logics to support reasoning about adversarial properties that specify the behavior of a known program (an oracle) with respect to an unknown program or environment (the adversary). These properties are important concepts in fields such as security or privacy.
Also, in this study, Aguirre considers other related topics. First he looks into proving properties of Markov chains. Many of these properties are inherently relational (e.g., stochastic dominance, recurrence, transience). He adapts the Guarded Lambda Calculus, and the Guarded HOL -a language and logic to reason about infinite streams-, to his setting by extending them with probabilities and developing a relational logic on top of Guarded HOL. Second, he presents a relational logic for higher-order probabilistic programs that is not lifting-based. This requires an extension of the assertion language and an axiomatization of probability theory in the base logic. Finally, Alejandro develops a predicate transformer to reason about expected sensitivity of probabilistic programs.
With this work, the researcher Alejandro Aguirre manages to make a leap in the world of privacy and computer security. He has made several achievements that allow us to learn more about the operation of some programs with probabilistic behaviour.
The Secretary of State for Digitisation and Artificial Intelligence, Carme Artigas, the Regional Minister for Science, Universities and Innovation (CM), Eduardo Sicilia, and the Director General for Research and Technological Innovation, María Luisa Castaño have visited the IMDEA Software Institute.
The director of the Institute, Manuel Carro, the deputy director, Juan Caballero, and the former director, Manuel Hermenegildo, received the personalities and took them on a tour of the facilities in which they were not only shown the building but also the cutting-edge research work.
The researcher Aleks Nanevski opened the welcome session in which he briefly explained the history of the Institute and the importance of software research. The committe was directed to the third floor where Manuel Hermenegildo spoke about green computing, and Dario Fiore and Ignacio Cascudo about cryptography, a very important part of the Institute. Juan Caballero spoke to them about computer security and the research being done at the Institute.
The visit continued with a walk through the floor to the Happening area where Alessandra Gorla briefed them on computerised testing as well as the projects she is involved in, and finally, Alexey Gotsman gave them a glimpse about distributed systems.
After the sessions with some of the institute's researchers, the visit continued to a meeting room where a private meeting was held to discuss important topics and strategies for attracting and retaining talent as well as technology transfer to the Industry.
The Secretary of State of Digitization and #AI, @carmeartigas (@SEDIAgob), @edsicilia and @CastanoMluisa, from the Council of Science, Universities and Innovation (@ComunidadMadrid) have visited us today. @IMDEAInstitutes pic.twitter.com/8utrgx8XeT— IMDEA Software Institute (@IMDEA_Software) March 2, 2021
The researcher of the IMDEA Software Institute, Niki Vazou, has been elected as part of the members of the board of the Haskell Foundation. It is the first time the Foundation decides to create a Board of Directors, so the presence of Vazou is historic.
The Haskell Foundation Board of Directors are responsible for managing and setting the direction of the Haskell Foundation. HF's current board will serve on an interim basis during the launch phase and will manage the establishment of the first full board in early 2021.
Haskell is not “just another programming language”: it embodies a radical and elegant attack on the entire enterprise of writing software. It profoundly influences the world of software for the better. The Haskell Foundation (HF) is an independent, non-profit organization dedicated to broadening the adoption of Haskell, by supporting its ecosystem of tools, libraries, education, and research.
It is not a secret that Niki's research interests include refinement types, automated program verification, and type systems and her goal is to make theorem proving a useful part of mainstream programming. Liquid Haskell is an SMT-based, refinement type checker for Haskell programs that has been used for various applications ranging from fully automatic light verification of Haskell code, e.g., bound checking, to sophisticated theorem proving, e.g., non-interference.
Manuel Hermenegildo, Distinguished Professor at the IMDEA Software Institute, has been appointed for a second term as Chairman of the Scientific Board of INRIA, the French National Institute for Research in Computer Science and Automation (Institut national de recherche en informatique et en automatique). He will carry out that role for a new period of three years.
INRIA is a French national public research institution focused on computer science and applied mathematics. It comprises 8 research centers (in Bordeaux, Grenoble-Inovallée, Lille, Nancy, Paris-Rocquencourt, Rennes, Saclay, and Sophia Antipolis) and employs more than 3800 people, including 1300 researchers, 1000 Ph.D. students, and 500 postdocs.
The INRIA Scientific Board provides guidance on the major aspects of INRIA's scientific policy, including the development of the research centers and teams, and the appointment and renewal of directors, in agreement with the Board of Directors.
The researchers Dario Fiore (IMDEA Software Institute), Aikaterini Mitrokotsa (Chalmers University of Technology), Luca Nizzardo (Protocol Labs Research) and Elena Pagnin (Lund University) receive the 2020 Premium Award for Best Paper in the IET (The Institution of Engineering and Technology) for the paper: "Multi-Key Homomorphic Authenticators."
The technological innovations offered by modern IT systems are changing the way digital data is collected, stored, processed, and consumed. As an example, think of an application where data is collected by some organisations (e.g. hospitals), stored and processed on remote servers (e.g. the Cloud) and finally consumed by other users (e.g. medical researchers) on other devices. On the one hand, this computing paradigm is very attractive, particularly as data can be shared and exchanged by multiple users. On the other hand, it is evident that in such scenarios, one may be concerned about security: while the users that collect and consume the data may trust each other (up to some extent), trusting the Cloud can be problematic for various reasons. More specifically, two main security concerns to be addressed are those about the privacy and authenticity of the data stored and processed in untrusted environments.
While it is widely known that privacy can be solved in such a setting using, e.g. homomorphic encryption, in this work, the authors focus on the orthogonal problem of providing authenticity of data during computation. Towards this goal, their contribution is on advancing the study of homomorphic authenticators (HAs), a cryptographic primitive that has been the subject of recent work.
Homomorphic authenticators (HAs) enable a client to authenticate a large collection of data elements and outsource them, along with the corresponding authenticators, to an untrusted server. At any later point, the server can generate a short authenticator vouching for the correctness of the output y of a function f computed on the outsourced data. The notion of HAs studied in prior work, however, only supports executions of computations over data authenticated by a single user.
In this paper, the authors introduce and formally define multi‐key HAs, they propose a construction of a multi‐key homomorphic signature based on standard lattices and supporting the evaluation of circuits of bounded polynomial depth, and they provide a construction of multi‐key homomorphic MACs based only on pseudorandom functions and supporting the evaluation of low‐degree arithmetic circuits.
In conclusion, this paper provides an innovative solution through the notion of multi‐key HAs. This primitive guarantees that the corruption of one user affects the data of that user only, but does not endanger the authenticity of computations among the other (un‐corrupted) users of the system. Moreover, the proposed system is dynamic, in the sense that compromised users can be assigned new keys and be easily reintegrated.
This paper is an extended version (with additional results and detailed proofs) of the paper "Multi-Key Homomorphic Authenticators" presented by the same authors at ASIACRYPT 2016.
The researchers Álvaro Feal (IMDEA Networks Institute), Paolo Calciati (IMDEA Software Institute), Narseo Vallina-Rodríguez (IMDEA Networks Institute), Carmela Troncoso (Spring Lab EPFL), and Alessandra Gorla (IMDEA Software Institute) have won the "Emilio Aced Award for the Research and Personal Data Protection" given by the Spanish data protection agency (AEPD), for the paper "Angel or Devil? A Privacy Study of Mobile Parental Control Apps."
Parental control apps are used by parents to monitor the use that their children make of their mobile phones, and to block access to certain features. These apps are highly intrusive by definition, as they can track the actions and movements of the children’s phone (and thus of the child). Therefore, the use of parental control apps can have implications on the privacy of both children and parents.
Existing recommendations by official bodies (such as SIP4 by the European Commission) do not take privacy into consideration, benchmarking only features such as price, capabilities, or usability. To assess such privacy risks, Álvaro, Paolo, Narseo, Carmela and Alessandra relied on a combination of static and dynamic analysis to study 46 parental control apps.
In their work, the researchers found that almost 75% of the apps contain data-driven third-party libraries for secondary purposes (namely advertisement, social networks, and analytic services) and that 67% of the apps share private data without user consent, including apps recommended by public bodies, such as IS4K (Internet Segura For Kids by INCIBE).
The researchers have presented the first multi-dimensional study of the parental control apps ecosystem from a privacy perspective. With their findings they open a debate about the privacy risks introduced by these apps. Does the potential of parental control apps for protecting children justify the risks regarding the collection and processing of their data? This is worrisome, as current legislation (such as the GDPR) protects children’s data from being accessed without clear parental consent. So, given the potential risks of this type of software, they recommend parents to rely on non-technical solutions when possible and to have privacy in mind when choosing one of these applications.
They believe that public bodies should take privacy into account when recommending a given parental control app to raise awareness and encourage developers to follow privacy-by-design principles. The researchers from the IMDEA Software Institute, IMDEA Networks Institute and Spring Lab EPFL stress that it is fundamental to complement current benchmarking initiatives with a security and privacy analysis to help parents to choose the best application while taking these aspects into consideration.
The former researcher of the IMDEA Software Institute, Platon Kotzias, defended his thesis: “A Systematic Empirical Analysis of Unwanted Software Abuse, Prevalence, Distribution, and Economics” in 2019, directed by the Associate Professor, Juan Caballero. Today he works at NortonLifeLock on a wide range of system security topics including malware detection on Android and Windows, application of AI on security topics, and network security.
This month the UPM has resolved the two winners of the Extraordinary Award and Platon's thesis is one of them. In which he investigates how Potentially Unwanted Programs (PUP) can pose significant risks to users’ security and privacy. In particular, he analyzed in both breadth and depth the PUP abuse, prevalence, distribution, and economics.
His PhD shed light on various unknown facets of PUP that affected millions of Internet users. His work has been published in top-tier security conferences like Usenix Security, ACM CCS, IEEE Security & Privacy, and NDSS Symposium.
The four contributions of the thesis
Platon Kotzias performs a systematic study on the abuse of Windows Authenticode code signing by PUP and malware. Building an infrastructure that classifies potentially malicious samples as PUP or malware and using this infrastructure to evaluate 356K samples. He also evaluates the efficacy of Certification Authority (CA) defenses such as identity checks and revocation. CA revocations were equally low for both malware and PUP, so, he concludes that current CA defenses are largely ineffective for PUP.
He measured the prevalence of unwanted software on real consumer hosts using telemetry from 3.9 million hosts. He found PUP installed in 54% of the hosts in their dataset. They also analyzed the commercial pay-per-install (PPI) service ecosystem showing that commercial PPI services play a major role in the distribution of PUP.
In his thesis, Platon performed an analysis of enterprise security and measured the prevalence of both malware and PUP on real enterprise hosts. He used AV telemetry collected from 28K enterprises and 67 industry sectors with over 82M client hosts. Almost all enterprises, despite their different security postures, encounter some malware or PUP in a three year period.
And lastly, he performed an analysis of PUP economics. He proposed a novel technique for performing PUP attribution. Then, he used it to identify the entities behind three large Spanish-based PUP operations and measure the profitability of the companies they operate. The analysis showed that in each operation a small number of people manages a large number of companies, and that the majority of them are shell companies. In the period 2013–2015, the three operations have a total revenue of 202.5M euros and net income of 23M euros. Finally, he observed a sharp decrease on both revenue and income for all three operations starting mid-2014. So, he concludes that improved PUP defenses deployed by various software and security vendors significantly had an impact on the PPI market.
The European Research Council (ERC) announced today the awardees of its latest Consolidator Grant call for mid-career researchers. Its funding is part of the EU's current research and innovation programme, Horizon 2020, and worth in total €655 million.
The ERC has granted 327 Consolidator Grants in 2020 to researchers from 23 countries, of which 22 were given to Spanish proposals (consult statistics). The proposal of the IMDEA Software Institute researcher, Dario Fiore, with the project "Cryptography for Privacy and Integrity of Computation on Untrusted Machines (PICOCRYPT)" is one of them.
Dr. Fiore's proposal, planned for five years, has a budget of €2 million, which will allow him to consolidate his research team and make far-reaching advances. PICOCRYPT becomes the third ERC grant awarded to researchers from the IMDEA Software Institute.
The PICOCRYPT project
Due to phenomena like the ubiquity of the Internet and cloud computing, it is increasingly common to store and process data on third-party machines. In spite of its attractive aspects, this trend raises a number of security concerns, including: How to ensure that the results computed by third parties are correct (integrity) and no unauthorized information is leaked (privacy)? The current way to deal with these problems is to trust third parties under legislation guarantees. This approach assumes that third-party machines stay honest all time, even if they get hacked! This is unrealistic and contradicted by the numerous security incidents that are regularly reported.
Instead, Dr. Fiore's view is that it should be possible to store and process data on untrusted machines without risking for privacy and integrity and without the need of trusting these machines. Recent trends in cryptography promise solutions to realize this vision but the existing generation of protocols is limited due to its high costs and its poor support to emerging applications such as data stream processing. The grand challenge of this project is to invent a new generation of cryptographic protocols for commputing securely on untrusted machines in a way that is cost-effective and suitable for future application scenarios.
The solutions provided by the PICOCRYPT project will have the potential to generate a paradigm shift in the way privacy and integrity are ensured and will have an impact on the world of information technology by making delegated computing more secure not only for citizens but also for public and private organizations that, due to current risks, may give up using these services.
The researchers František Farka, Aleksandar Nanevski, Anindya Banerjee (from the IMDEA Software Institute), Germán Andrés Delbianco (Nomadic Labs), and Ignacio Fábregas (Universidad Complutense de Madrid) have recently published "On Algebraic Abstractions for Concurrent Separation Logics", that has been accepted at POPL 2021.
Concurrent separation logic is a logic for verification of stateful programs. This logic is distinguished by transfer of state ownership upon parallel composition of threads. The semantics ownership transfer is given by the algebraic structure of partial commutative monoids(PCMs). Extant research considers ownership transfer primarily from the logical perspective while comparatively less attention is drawn to the symbolic manipulation on the level of specifications expressed in the assertion language.
This paper provides an algebraic formalization of assertion language for ownership transfer in concurrent separation logic by means of structure-preserving partial functions (i.e., morphisms) between PCMs, and an associated notion of separating relations.That is, when verifying software, they can assert specifications in symbolic languages of standard mathematics; the only concession they are forced to is relaxation from total domains to partial ones.
Morphisms, that is structures preserving maps, are a standard concept in algebra and category theory. However, morphisms haven't seen ubiquitous use in separation logic before. Separating relations are binary relations that generalize disjointness and characterize the inputs on which morphisms preserve structure. The two abstractions facilitate verification by enabling concise ways of writing specs, by providing abstract views of threads' states that are preserved under ownership transfer, and by enabling user-level construction of new PCMs out of existing ones.
The presented work constitutes a novel approach to assertion language of separation logics as the algebra of PCMs, their morphisms and constructions has not been considered before in this context.
IMDEA Software Institute researcher, Manuel Hermenegildo, gives the Opening Invited Talk at the 27th Static Analysis Symposium (SAS'20), on "Cost Analysis of Smart Contracts via Parametric Resource Analysis," work co-authored with Víctor Pérez, Maximiliano Klemen, Pedro López-García and José Francisco Morales.
This line of research is motivated by the fact that, in blockchains, contract execution and storage are replicated across large numbers of nodes, and this makes resource consumption an important concern. The few cost analyzers that exist for smart contracts are for specific platforms and languages. However, blockchain platforms present significant variability, also over time.
Parametric Resource Analysis (also referred to as User-Defined Resource Analysis) is a generic approach, proposed by the IMDEA Software Institute team, for developing analyzers that infer safe bounds on different resources and with different resource models. In the talk, Manuel Hermenegildo reviews this approach and explores its application to the static inference of gas and storage consumption bounds for smart contracts, reporting on a concrete case study: developing an analyzer for the Tezos platform and its Michelson language. The results show that the approach is an effective method for the rapid development and maintenance of cost analyzers for smart contracts.
The Parametric Resource Analysis approach was awarded the 10 year Test-of-Time Award at the 2017 International Conference on Logic Programming, the premier conference in the area.
IMDEA Software's CiaoPP framework implements this approach and allows its application to different programming languages, by translation into a Horn clause-based intermediate representation.
The series of International Static Analysis Symposia (SAS) serves as the primary venue for presentation of theoretical, practical, and application advances in this area. This edition of SAS is co-located with SPLASH'20 in an online form, coordinated from Chicago, USA, from November 18 to November 20, 2020. SPLASH embraces all aspects of software construction and delivery, to make it the premier conference on the applications of programming languages - at the intersection of programming languages and software engineering.
The associated work is conducted in the context of the collaboration of the Tezos foundation and Nomadic labs with the IMDEA Software Institute.
The 2020 edition of the REDIMadrid Conference has been completely virtual due to the COVID-19, but efforts have been made to make the conference very interesting, shorter in order to continue to attract a very determined audience.
Blanca Gutiérrez, Communication Manager of the IMDEA Software Institute, began the conference with a brief introduction and was followed by Manuel Carro, Director of the IMDEA Software Institute, who gave the conference's opening speech.
Manuel, spoke about the origin of the network as well as high-speed networks that offer services to the educational and scientific community. In this sense, he stated that teleworking, forced by the arise of the pandemic, would not have been possible without fibre optic networks such as REDIMadrid. "The leap into the digital world and into education has come to stay despite the fact that regulations must also be updated" he confirmed.
"The state of REDIMadrid. Present and Future" was the first presentation, given by César Sánchez, director of REDIMadrid and Associate Research Professor at the IMDEA Software Institute, in which he commented that REDIMadrid is the last mile of the RedIRIS network in Madrid as part of the European GEANT network.
David Rincón, Coordinator of REDIMadrid, spoke about the Denial of Service (DDoS) attacks in the educational environment that have resulted with the tendering of a software to mitigate these attacks. "This is a new service offered by REDIMadrid which has had to be adjusted to the change in profile caused by COVID-19" he said of the GENIE tool. The traffic is mitigated before it reaches the institutions, so the network's clients are protected.
The following talk: "The Madrid Quantum Network", was given by Vicente Martín, professor of the Computer Science Faculty, UPM. His presentation was based on the quantum network that is being deployed in Madrid as part of the OpenQKD project. "Quantum computing is characterised by the basic information unit Qubit. Qubits communication consists of the propagation of photons and, when these are in transit, they cannot be touched without modifying their characteristics, for this reason they cannot be intercepted in transit and this is what gives the technology total security" confirms Vicente.
After the talk on quantum communications came the WhiteBox colloquium in which the following took part: Diego Nuevo, Network & Data Center Arquitect at Axians; Víctor López, technology expert in the General Directorate of Systems and Networks at Telefónica; and Óscar Rebollo, engineer at REDIMadrid. The situation of integration, costs and support of the whiteboxes was discussed, as well as the state of penetration of this equipment in the clients' networks, exemplified by the TIP project (Telecom Infra Project).
The conference continued with the talk "The Lockdown Effect: Implications of the COVID-19 Pandemic on Internet Traffic", based on a publication that will be presented soon and whose authors are Juan Tapiador, professor of computer science at UC3M, and Narseo Vallina-Rodríguez, Research Assistant Professor at the IMDEA Networks Institute. REDIMadrid has contributed to this study by providing traffic data.
The next to participate was Marta Vázquez, from INTECCA-UNED, who presented the AVIP application. "From COVID-19, videoconferencing has become compulsory at the UNED and thanks to the application's scalable architecture, it has been possible to absorb the large increase in traffic, which has peaked at over one hundred thousand users on some days".
And finally, Gibran Gómez, researcher at the IMDEA Software Institute, gave a talk on "Malicious TLS Traffic Detection using Unsupervised Machine Learning". According to Gibran "there are few protocols that send clear information, so attacks on protocols that use encryption such as TLS are beginning to increase. Machine Learning (ML) techniques are used to detect and combat MITM and malware attacks and the system developed detects them and generates alerts".
She focuses in this thesis on the models of finite-state automata, pushdown automata and context-free grammars. These models have been proved useful for a wide number of applications such as program verification, natural language processing tasks or digital-image compression techniques. These applications strongly rely on language-theoretical notions where, still today, many questions are open.
The goal of this thesis is to give new theoretical perspective on a collection of open problems, that are at the core of classical automata constructions and well-established algorithms.
The underlying mathematical tool to approach these questions are equivalence relations on words as abstractions of languages. So, she studies three main questions:
In this thesis, she aims to get a better understanding of the language-theoretical basis of the double-reversal method and its connection with the partition-based techniques. As a result, we provide a uniform framework of deterministic automata constructions based on finite-index equivalences on words that allows us to give a new simple proof of the double-reversal method and shed light on the relation between this algorithm and the partition-based techniques.
Her main contribution is to provide an infinite family of PDAs defined over a singleton alphabet that allows her to extract lower bounds on the number of grammar variables of the smallest CFG.
To sum up, "in this dissertation we leverage equivalences on words as abstractions of languages. More pointedly, these abstractions are regular approximations of languages. Our results regarding finite-index congruences encourages the study of other kinds of regular approximations of context-free languages and the use of our framework to define congruence-based automata constructions for their finite representation", appointed Elena. On the other hand, her work on the Parikh equivalence assumption shows that, despite being a relaxed version of language equivalence that enables the analysis of certain complex systems, when comparing PDAs against CFGs the situation is not different to that of language equivalence. And also, sets the basis for future directions on the extension of Parikh's Theorem to weighted automata.
The researchers Zsolt István (IMDEA Software Institute), Kaan Kara, (Oracle Labs), and David Sidler (Microsoft Corporation) have published the book "FPGA-Accelerated Analytics: From Single Nodes to Clusters".
Today datacenters that host data-intensive applications used in online services and machine learning need to store and process data that increases at an exponential rate. Data processing and management applications have become increasingly distributed and this has lead to new data movement bottlenecks at various levels of software and hardware architecture.
The authors survey recent research on using reconfigurable hardware accelerators, namely, Field Programmable Gate Arrays (FPGAs), to accelerate analytical processing. Such accelerators are being adopted as a way of overcoming the recent stagnation in CPU performance because they can implement algorithms differently from traditional CPUs, breaking traditional trade-offs.
Zsolt, Kaan and David discuss the benefits of using FPGAs in the context of analytical processing, both as an accelerator within a single node database and as part of distributed data analytics pipelines. They also present guidelines for accelerator design in both scenarios, as well as, examples of integration within full-fledged Relational Databases.
Finally, they highlight future research challenges in programmability and integration, and cover architectural trends that are propelling the rapid adoption of accelerators in datacenters and the cloud.
The researchers Alfredo Di Napoli, Andres Löh (both from Well-Typed LLP), Ranjit Jhala (University of California at San Diego) and Niki Vazou, from the IMDEA Software Institute have presented: “Liquid Haskell as a GHC Plugin” at the Haskell Implementors’ Workshop (HIW 2020) in ICFP 2020.
Liquid Haskell is a system that extends GHC with refinement types. Constraints arising from the refinement types are sent to an external automatic theorem prover such as z3. By employing such additional checks, one can express more interesting properties about Haskell programs statically.
Up until now, Liquid Haskell has been a separate executable that uses the GHC API, but would run on Haskell files individually and just say “SAFE” or “UNSAFE”. If “SAFE”, one could then proceed to compile a program normally.
Recently, the researchers have rewritten Liquid Haskell to now be a GHC plugin. The main advantages of this approach are:
When checking source files, Liquid Haskell requires information about the constraints already established for dependent libraries. Previously, these had to be hand-distributed for selected modules with Liquid Haskell itself. Now, they become part of normal GHC interface files and can be distributed for arbitrary user packages via Hackage.
In this work, the researchers present the Liquid Haskell plugin workflow and why they think it is superior to the old approach. They also discuss the implementation of the plugin: it is interesting because it does not neatly fit into the plugin categories currently provided. Morally, Liquid Haskell typechecks the code, but in order to generate constraints to feed to the prover, it must access (unoptimised!) core code. They explain the final design, and some of the iterations they needed to get there.
The researchers Pierre Ganty, Elena Gutiérrez and Pedro Valero have recently published "A Quasiorder-based Perspective in Residual Automata" presented at MFCS 2020 (Mathematical Foundations of Computer Science) that took place from the 24th-28th of August. The three researchers of the IMDEA Software Institute propose a different view on a class of finite-state machines of great relevance in practice, the so-called "Residual Automata".
To give a little bit of context, residual automata are classical finite-state automata (FSAs for short), i.e., transition systems with a finite number of states that are used to represent the so-called regular languages, one of the most studied objects in formal language theory.
Actually, finite-state automata are finite representations of regular languages, and this might not be illuminating but it is rather helpful when the languages they represent are infinite!
Going back to our objects, residual automata, among the general FSAs, enjoy interesting properties that make them useful in applications such as grammar inference.
The main goal of grammar inference is to find a target language using a finite set of examples of words in the language. In other words, grammar inference is a machine learning technique by means of which we learn a (possibly infinite) language of words given only a finite number of them.
In this context, residual automata are useful tools as it has been proven that they can represent very concisely (and finitely, since they are FSAs) the target language.
In this paper, they study the properties of residual automata from a theoretical point of view.
Namely, we use quasiorders as a mathematical tool to give a new perspective on the construction of residual automata. Quasiorders are relations between the elements of a set satisfying some properties. For instance, given the set of all natural numbers N, the relation ≤, which relates two elements x and y if x ≤ y, is a quasiorder on N.
In this work, they define quasiorders on words and use them to construct residual automata. By using different quasiorders we construct different residual automata, including the minimal one for some given language.
Concretely, we present a new residualization operation and a generalized Brzozowski's method for building the minimal residual automaton for a given language. We also leverage this technique to offer a new perspective on NL*, an online learning algorithm for residual automata.
Secret sharing schemes enables a dealer to split a secret into a set of shares, in such a way that certain authorized subsets of shareholders can reconstruct the secret, whereas all unauthorized subsets cannot.
Non-malleable secret sharing schemes (Goyal and Kumar, STOC 2018) additionally require that if the shares have been maliciously modified then the reconstructed secret is completely unrelated one.
The researchers Gianlunca Brian (Sapienza, University of Rome), Antonio Faonio (IMDEA Software Institute), Maciej Obremski (National University of Singapore), Mark Simkin (Aarhus University), Daniele Venturi (Sapienza, University of Rome) have worked jointly to create "Non-Malleable Secret Sharing against Bounded Joint-Tampering Attacks in the Plain Model" paper that was accepted at Crypto 2020.
In their work, they construct non-malleable secret sharing schemes secure against attackers that can maliciously modify the shares more than once in the so-called joint-tampering model.
In particular, assuming one-to-one one-way functions, they obtain:
– A threshold secret sharing scheme secure under attacks where the attacker commits to a partition of the shares, and keeps tampering jointly with the shares within such a partition (so-called selective partitioning).
– A secret sharing scheme for general access structures which tolerates joint tampering with subsets of the shares of size O(√log n), where n is the number of parties. The scheme is secure even if the attacker is allowed to adaptively change the partitions (so-called semi-adaptive partitioning).
Their research lies a new technique showing that every one-time statistically non-malleable secret sharing against joint tampering is in fact leakage-resilient non-malleable (i.e., the attacker can leak jointly from the shares prior to tampering). This may be of independent interest, and in fact they show it implies lower bounds on the share size and randomness complexity of statistically nonmalleable secret sharing against independent tampering.
The researcher from the IMDEA Software Institute Pedro Valero, supervised by Pierre Ganty, defended his PhD thesis with the title “On the use of Quasiorders in Formal Language Theory”, on the 20th of July. He submitted his thesis as partial fulfillment of the requirements for the degree of Doctor of Philosophy in Software, Systems and Computing.
Quasiorders on words, i.e. binary relations between words, have proven useful for reasoning about formal languages from a theoretical perspective. For instance they have been used to characterize the class of regular languages and for showing that all maximal solutions of certain systems of inequalities on languages are regular.
In his work, Pedro shows that quasiorders also have practical applications by placing them at the core of several efficient algorithms.
More precisely, in his thesis, Pedro uses quasiorders on words to offer a new perspective on two well-studied problems from Formal Language Theory: deciding language inclusion, with applications to searching on compressed text, and manipulating the finite automata representations of regular languages.
The Language Inclusion Problem
The thesis considers the language inclusion problem L1 ⊆ L2, where L1 is regular or context-free and L2 is regular.This problem is solved by checking whether an over-approximation of L1 is included in L2, showing that the language inclusion problem is decidable whenever the over-approximating function satisfies a completeness condition (i.e. its loss of precision causes no false alarm) and prevents infinite ascending chains (i.e. it guarantees termination of least fixpoint computations).
Such over-approximation of L1 is defined using quasiorder relations on words where the over-approximation gives the language of all words “greater than or equal to” a given input word for that quasiorder. In his thesis, Pedro presents a range of quasiorders in order to systematically design decision procedures for different language inclusion problems such as regular languages into regular languages or into trace sets of one-counter nets and context-free languages into regular languages.
Some of the obtained inclusion checking procedures correspond to well-known algorithms, like the so-called antichains algorithms, while others correspond to novel algorithms such as the presented greatest fixpoint language inclusion check, which relies on quotients of languages.
Searching on Compressed Text
Secondly, the thesis instantiates the quasiorder-based framework for the scenario in which L1 consists on a single word generated by a context-free grammar and L2 is the regular language generated by an automaton. The resulting algorithm can be used for deciding whether a grammar-compressed text contains a match for a regular expression.
This algorithm is then extended in order to count the number of lines in the uncompressed text that contain a match for the regular expression. Remarkably, this extension runs in time linear in the size of the compressed data, which might be exponentially smaller than the uncompressed text.
Furthermore, Pedro's thesis proposes efficient data structures that yield optimal complexity bounds and an implementation –zearch– that outperforms the state of the art, offering up to 40% speedup with respect to highly optimized implementations of the standard decompress and search approach.
Residual Finite-State Automata
The last technical contribution of this thesis is a framework of finite-state automata constructions based on quasiorders over words that provides new insights on residual finite-state automata (RFA for short).
This framework is used to present a generalization of the double-reversal method for RFAs along the lines of the one for deterministic automata and to offer a new perspective on NL∗, an on-line learning algorithm for RFAs. These results evidence that quasiorders are fundamental to residual automata in the same way congruences are fundamental for deterministic automata.
The researcher of the IMDEA Software Institute, Pepe Vila, has sucessfully defended his PhD thesis titled: "Learning secrets and models from execution time". Professor Boris Köpf (on leave researcher of the Institute and researcher of Microsoft Research Lab at Cambridge) was his advisor.
In his work he studies some of the problems arising on computer systems that leak information through execution time. They study several instances of how these leaks can be used to both learn secrets—of a confidential computation—and models—of an underlying component—, providing examples that violate previous assumptions about systems’ security or about the attackers’ capabilities.
He studies in particular, time leakage under three different scenarios, providing multiple independent contributions in each of them:
• First, he shows that event-driven software systems are susceptible to side- channel attacks. The key observation is that event loops form a resource that can be shared between mutually distrusting programs. Hence, con- tention of this resource by one program can be observed by the others through variations in the time the latter processes take for dispatching their events. We exploit two different shared event loops in the Chrome web browser, and use the information obtained in three different attacks: for web page fingerprinting, for keystroke detection, and for a cross-origin covert channel.
• Then, he reveals that the contributions are both theoretical and practical. On the theoretical side, we formalize the problem of finding minimal eviction sets, a key primitive for several microarchitectural attacks, and devise novel algorithms that improve the state-of-the-art from quadratic to linear. On the practical side, we perform a rigorous empirical analysis that exhibits the conditions under which our algorithms succeed or fail.
• Finally, he presents a practical end-to-end solution for inferring deterministic cache replacement policies using off-the-shelf techniques for automata learning and program synthesis. The enabling contribution is a chain of two abstractions: a clean interface to the hardware cache replacement poli- cies based on timing measurements on a silicon CPU; and a mapper that exposes a membership oracle to the cache replacement policy abstracting away the details regarding cache content management.
In conclusion, the results of Pepe Vila's thesis constitute an evidence that better models and quantification methods -for both software and hardware systems-, are required in order to reason about the soundness and trade-offs of security countermeasures; and provide a basis for principled countermeasures against, or paths for further improving the efficiency of, several side channel attacks.
The 5th edition of the Mutua Universal Innovation and Health Awards recognizes innovation for the benefit of people and its awards are intended to distinguish and reward the work of those companies that are highly committed to health promotion and have carried out innovative projects or actions that represent an improvement in the quality of life and health of their workers.
The award-winning action 'IMDEA Software ecoHealth' was born with the approach of the new headquarters of the IMDEA Software Institute in 2009 and since then has been developed and expanded over time, as well as with the invaluable collaboration of its own workers.
The main objectives of the action are: promote ecological awareness; facilitate integration in a multicultural environment; offer possibilities for work-life balance; and maintain a continuous conversation over time on matters of general interest in order to advance and innovate by pursuing constant improvement for the entire staff.
The IMDEA Software Institute provides facilities for its workers to lead healthy lives and exercise: it promotes cycling by providing the car park with its own space; it has a multi-purpose room next to the changing rooms where sports activities can be carried out; it has a breastfeeding room; and, among other things, it is a cardio-protected space that offers its staff training to be able to apply it if necessary.
In addition, the Institute is a research centre committed with the environment. It has parking spaces with electric chargers, 100% ecological cleaning products are used and recycling is actively encouraged, and the automation system turns the building into an efficient space (Energy Class B).
The researchers Ignacio Cascudo (IMDEA Software Institute) and Bernardo David (IT University of Copenhagen) have recently published "ALBATROSS: publicly AttestabLe BATched Randomness based On Secret Sharing".
ALBATROSS is a family of multiparty randomness generation protocols with guaranteed output delivery and public verification that allows to trade off corruption tolerance for a much improved amortized computational complexity.
Their basic stand alone protocol is based on publicly verifiable secret sharing (PVSS) and is secure under in the random oracle model under the decisional Diffie-Hellman (DDH) hardness assumption. They also address the important issue of constructing Universally Composable randomness beacons (that can be used in more complex environments), showing two UC versions of Albatross: one based on simple UC NIZKs and another one based on novel efficient "designated verifier" homomorphic commitments. Interestingly this latter version can be instantiated from a global random oracle under the weaker Computational Diffie-Hellman (CDH) assumption.
An execution of ALBATROSS with n parties, out of which up to t = (1/2 − ε) · n are corrupt for a constant ε > 0, generates Θ(n^2) uniformly random values, requiring in the worst case an amortized cost per party of Θ(log n) exponentiations per random value. On Cascudo and David paper they significantly improve on the SCRAPE protocol, which required Θ(n^2) exponentiations per party to generate one uni- formly random value. This is mainly achieved via two techniques: first, the use of packed Shamir secret sharing for the PVSS; second, the use of linear t-resilient functions (computed via a Fast Fourier Transform-based algorithm) to improve the randomness extraction.
The main application of these protocols is in proof-of-stake blockchains, which, every certain period of time, requires to elect a "leader" among the users of the protocol, and where this selection must not be possible to be biased, and the correctness of this process needs to be able to be verified publicly.
The IMDEA Software Institute researchers Pepe Vila, Pierre Ganty and Marco Guarnieri, and Boris Koepf, from Microsoft Research, are the authors of the recent paper “CacheQuery: Learning Replacement Policies from Hardware Caches” accepted at the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2020).
Caches are small and fast memories that sit between the CPU and the main memory (DRAM) of computers. Their main goal is to speed up computations by reducing the time it takes to load and store data, and since their capacity is limited, they must anticipate which data is going to be used in the near future. The better this prediction, the better the performance.
Thus, the cache replacement policy is the logic that decides which data is kept in the memory cache and which is replaced to make room for more useful data. It is a critical component for the performance of modern computers.
In most modern processors these policies are not documented, and since they have a huge performance impact, the absence of precise models makes it very difficult to predict and analyze the behavior and security of programs.
“We lack precise models of our hardware. With our approach, we close this gap, and we allow other people to understand how the policy optimizes certain workloads, so that they can predict the timing behavior of critical systems (i.e., cars or planes), calculate limits on the information leakage of cryptographic programs, or write more accurate hardware simulators” comments Pepe Vila, predoctoral researcher of the IMDEA Software Institute.
Transparency, is the first step towards improving the security and safety of computer systems. In this sense, the researcher of the Institute, Marco Guarnieri, says that: “microprocessors and memories are central components of our computing infrastructure. Security vulnerabilities in these components may result in attacks affecting any program running on top of them. To assess and study the security of microprocessors and memories, researchers need high-level models documenting and describing their behaviors. Unfortunately, many crucial details of how these components work are undocumented. We see our research as a first step towards automatically generating such high-level models from hardware measurements and, ultimately, towards more secure systems”.
Through this partnership, the IMDEA Software Institute and BBVA have created a joint framework to research the use of this technology in the development of digital solutions that make it possible to harness data’s potential while also ensuring that users’ data remain private, anonymous and secure.
The agreement is especially relevant in the current context marked by the coronavirus crisis, which is demonstrating the importance of having robust systems to safeguard the privacy and security of data. On the one hand, this is due to the rise of cyber-attacks in recent weeks in which cyber criminals are taking advantage of users’ increased use of digital channels during the lockdown. And on the other, due to the interest sparked by the creation of COVID-19 tracking apps that respect data privacy, for which technologies of this kind could be very useful.
With this new partnership, both institutions will explore the application of a series of cryptographic techniques in the financial sector - techniques that make it possible for data to be shared and analyzed without exposing their content to third parties thanks to algorithms, protocols and encryption systems. These technologies, known as PET, or privacy-enhancing technologies are one of the fields in which the IMDEA Software Institute specializes, as well as one of the areas of interest that BBVA researches in its Research and Patent area.
Within this group of technologies, one that has the greatest potential and which will be the main subject of the new team’s study is zero knowledge proofs (ZKP). This technology uses cryptographic algorithms to make it easier to verify the accuracy of information, without having to share the data that comprise it. This way, it can help to create data-based solutions in which customers’ sensitive data is not exposed to third parties (as it is not necessary to share the data with them to prove that they are accurate).
Thanks to this agreement, both institutions are combining their capacities and knowledge in these areas. The goal is for the research to translate into tangible advances that make it possible to transfer the benefits of this technology to the financial sector, the corporate world, the scientific community and society as a whole.
To do so, in the first stage, the joint team will research how to solve some of the current challenges that the roll-out of this technology is still facing in order to share the results with the scientific community to foster progress in this discipline. Some of these challenges involve its integration with the current communication systems that companies are using, or the lack of common standards for the use of cryptographic protocols, which complicates its adoption on a large scale.
BBVA and the IMDEA Software Institute will also work on a series of real use cases identified in the financial sector, as well as the development of viable prototypes that can be incorporated in the digital products and services offered to BBVA customers.
The pre-doctoral researcher at the IMDEA Software Institute, Pepe Vila, participated at RootedCON 2020 last 7th of March giving a talk titled ‘The '80s never died: automata theory for reversing modern CPUs’ (view presentation). He explained his latest paper developed with the support and of the researchers Pierre Ganty and Marco Guarnieri, from IMDEA Software Institute, and Boris Köpf, from Microsoft Research, 'CacheQuery: Learning Replacement Policies from Hardware Caches' which reveals the previously unknown implementation of cache replacement policies used in modern processors.
Understanding the timing behavior of modern CPUs is crucial for optimizing code and for ensuring timing-related security and safety properties. Unfortunately, the timing behavior of modern processors depends on subtle and poorly documented details of their microarchitecture, which has triggered laborious efforts to reverse-engineer microarchitectural details. Cache replacement policies have received special attention, because they control the content stored in the memory hierarchy and hence heavily influence execution time.
In the paper, which has been accepted into PLDI'20 (Conference on Programming Language Design and Implementation), researchers from the IMDEA Software Institute and Microsoft Research present an end-to-end solution for automatically learning cache replacement policies from hardware time measurements. Their contribution is based on two main contributions: a tool, called CacheQuery, that provides an interface to any set in the cache hierarchy, freeing the user from having to deal with intricate details such as address translation, index mapping, interference from other cache levels or measurement noise; and, an algorithm, called Polka, that provides an abstract automaton for the cache replacement policy, and exploits various symmetries that make the automaton learning techniques applicable to the problem. In addition, they have been able to synthesize programs to automatically derive readable descriptions of the learned replacement policy.
In the experimental phase, their tests have been successful in learning several cache replacement policies used in Intel's latest processors, including two previously undocumented policies.
The 11th of February, on the occasion of the International Day of Woman and Girl in Science, the IMDEA Software Institute organised the conference 'Breaking Codes: Women and Girls in Science' with the support of various researchers from the Institute, as well as other centres on the Campus, such as the Center for Biomedical Technology CTB.
Blanca Gutiérrez, Communication Manager at the IMDEA Software Institute, was in charge of opening the conference in which she explained the importance of research for the advances in society and highlighted the need to promote scientific and research vocations in women and girls in a sector that is mainly masculine.
The first workshop was on reconstruction of neurons. Marta Domínguez and Marta Turégano, researchers at the CTB showed what a neuron is and helped the young women in the audience to differentiate between the different parts of a neuron: synapses, mitochondria, as well as spinal apparatus and myelin sheaths. In addition, they showed the software they use in their laboratory by which it automatically detects each differential element to be studied.
The cryptography workshop was led by three researchers from the IMDEA Software Institute: Anaïs Querol, Elena Gutiérrez and Isabel García. The first to open the workshop was Anaïs, who spoke about the origin of ciphered messages and how to encrypt and decrypt them. On the other hand, Isabel explained how to break mono-alphabetic ciphers. And finally, Elena delved into the workings of the enigma machine and how ciphers were broken at Bletchley Park.
After the workshops, the wikiton began. We divided the audience into groups and gave them a choice between seven Spanish scientists from different fields to create, through information provided, their page on Wikipedia.
The day ended with the 20 questions of the scientific trivial in which the knowledge acquired during the day was tested, as well as the general culture of the public.
The first blockchain hackathon for environmental action in Spain, organized by the IMDEA Software Institute and EIT Digital, whose awards were sponsored by the Tezos Foundation, ends with 11 award-winning participants from the three groups selected by the jury.
ChainrEaction had overall 26 participants, from 10 different countries. 10 of them were university students, 12 master students and 8 doctoral students. Almost 95% of the people respondents have interest (answering yes or maybe) in working at the IMDEA Software Institute. 50% of them punctuated 4 or 5 out of 5 according to their interest in a research-oriented career before chainrEaction, and this figure increased by 22,2% after the hackathon.
Three intensive days that began with presentations, and the introduction to the event given by Blanca Gutiérrez, Communication Manager, as well as Zsolt István, Assistant Research Professor, as part of the chanrEaction organizing committee of the IMDEA Software Institute. The morning continued with an inspiring talk by David Dao, Founder of Forest X, on "Decentralized Sustainability: Beyond the Tragedy of the Commons with Smart Contracts (and AI)".
Daniel Pérez, Chief Technology Officer at the Imperial College London, gave a tutorial on Ethereum as a mentor of chainrEaction that was a valuable, practical and challenging information for participants.
The second talk of the first day was given by Chrysa Stathakopoulou, a chainrEaction mentor and PhD student at ETH Zurich, on how to use and apply blockchain technology in businessess.
Meanwhile, Matteo Campanelli, postdoctoral researcher at the IMDEA Software Institute, organizer of chainrEaction and also a mentor, presented the second tutorial of the day on the chain code of Fabric Hyperledger and websites to interact with it.
During the last part of the day the participants presented their ideas, selected the seven teams that were formed and started coding.
The second day began with an interesting talk by Matej Šima, CEO os Stove Labs, who gave a beginner's guide to SmartContracts through Tezos technology. For the rest of the day participants had the opportunity to code practically the whole day, as well as to listen to the two EIT Digital Student Ambassadors, Renato Pinto and Cristina Ríos.
On the morning of the third day the seven groups were able to finish preparing their sustainable solutions. From 11 to 13 they presented their results to the jury made up of: the director of the IMDEA Software Institute, Manuel Carro; the director of the EIT Digital Co-Location Center, Jesús Contreras; the advisor to the Regional Ministry of Science, Universities and Innovation, Juan Jiménez; representative of the Blockchain Competence Center of Telefónica, María Teresa Nieto; the Head of Blockchain at iecisa, María Salgado; and the CEO of Stove Labs, Matej Šima.
At noon, "Reflections on blockchain at chanirEaction" began, an event opened to the public created within the framework of the hackathon, which featured different perspectives of blockchain through keynote talks given by international experts from industry and academia. Marko Vukolic, from IBM Research, Sara Tucci, from the CEA List Institute, and Jesús Ruiz, from the Spanish blockchain association, Alastria.
After the talks, Manuel Carro, as representative of the chainrEaction jury announced the winners of the three award categories and later proceeded to present the winning innovative ideas to the public.
The winner of the category "Most impressive proof of concept" was DONERO, an idea to give transparency to donations with a very strong focus. The category "Most viable pitch and business model" went to ENERGYCHAIN. A very well developed idea for transactions in the energy market. And finally, the award for "Most surprising use of blockchain" went to TRIPPIO, an idea to increase travel exchange using public transport.
The Director General of Research and Technological Innovation of the Madrid Regional Government, María Luisa Castaño, closed an event marked by the international youth talent that gave everything to create real wonders of sustainable solutions.
The IMDEA Software Institute and Nomadic Labs have signed a collaboration agreement to conduct research at the highest level in the Institute's research areas with the aim of contributing to the development of the Tezos ecosystem.
The Director General of Research and Technological Innovation of the Madrid Regional Government, María Luisa Castaño, and the Deputy Director of Research, Bárbara Fernández-Revuelta, attended the official signing ceremony between both institutions.
The director of the IMDEA Software Institute, Manuel Carro, the president of Nomadic Labs, Jérôme Chailloux, and the scientific director of Nomadic Labs, Michel Mauny, signed the collaboration agreement that implies that the Institute becomes a strategic partner of the Tezos ecosystem. "The Tezos project has forged numerous scientific collaborations at the best French and international level, as demonstrated by this collaboration with the IMDEA Software Institute. It is very important for us to prepare for the future of blockchain technologies, especially Tezos, by supporting open scientific research, the results of which will be public and therefore benefit the whole community. We are particularly pleased with the signing of this agreement between Nomadic Labs and IMDEA, which strengthens our ties with IMDEA and provides a framework for our collaboration", said Michel Mauny.
Manuel Carro stated that, "the agreement with Nomadic Labs for collaboration in the Tezos environment, the first to be signed in Spain, is an unparallel opportunity to contribute to a technology that is having difficulties to overestimate impact on society".
ElasTest is a Project funded by the European Union under the Horizon 2020 program. The main goal of the project is to provide a tool and an infrastructure to test end to end elastic applications. The modern cloud applications back ends are essentially elastic which means that they demand, they consume, they need more resources when they have, for example, more users, more access in the service, so this applications are notoriously difficult to test and to provide a software reliability which is a big challenge for mid-size and small enterprises. The project essentially is building an infrastructure to do this end to end testing and the different circumstances, for example: different users, many users at a time, different browsers, failures in the network and such, even failures in the components on the application itself.
The role of the IMDEA Software Institute in the project ElasTest has been to one, test security in the application and the other is to provide monitoring that allows to describe the test in an easier manner and to assess the test dynamically. César Sánchez ends the interview saying that: “All in all, I think that the ElasTest project has been very successful in both academic and in terms of developing the tool.”
Micro-architectural attacks, like the recently discovered Spectre and Meltdown attacks, exploit critical vulnerabilities in modern processors to compromise a system's security.
These attacks affect all modern general-purpose processors (such as those used in our computers). Concretely, they can bypass common security defenses at the software level by exploiting hardware side-effects.
In Marco Guarneri’s research, he developed tools for better understanding how micro-architectural attacks work. He then leverages this understanding to design new defense techniques against these attacks.
As a concrete example, Marco Guarnieri, José F. Morales and Andrés Sánchez, from the IMDEA Software Institute, Boris Köpf, from Microsoft Research, and Jan Reineke, from Saarland University recently developed SPECTECTOR, an automated technique for determining whether programs are vulnerable to a specific class of micro-architectural attacks called speculative execution attacks.
“Using Spectector, we detected subtle bugs in the way countermeasures against speculative execution attacks are placed by major compilers. These bugs may result in insecure programs or inefficient programs” ended Marco.
Niki Vazou, researcher at the IMDEA Software Institute, Martin A.T. Handley and Graham Hutton, from the University of Nottingham, UK have developed “Liquidate your Assets” a paper they presented to POPL2020 . You may find it here.
Liquid Haskell is an extension of Haskell’s Type system that allows annotating types with refinement predicates. It is great for ensuring correctness of code, but it can also be used to improve the performance of code.
Vazou, Handley and Hutton have designed and implement a system that allows Liquid Haskell to be used to formally reason about the resource usage of pure Haskell programs. Moreover, it supports reasoning about correctness and efficiency properties in a combined, uniform manner. "Our system takes the form of a library and requires no modifications or extensions to the compiler" comments Niki Vazou.
They have proven that their library’s approach to cost analysis is correct with respect to an underlying model of execution cost using the metatheory of Liquid Haskell.
In the end, they have demonstrated the applicability of their library on a wide range of case studies, ranging from standard sorting algorithms to sophisticated relational cost properties.
Luca Nizzardo, was a PhD student of the IMDEA Software Institute and his thesis “Cryptographic Techniques for the Security of Cloud and Blockchain Systems” defended in 2018 was directed by the Associate Professor, Dario Fiore. Nowadays he works for Protocol Labs helping to build protocols, systems, and tools to improve how Internet works.
This month the UPM has resolved the two winners of the Extraordinary Award and Luca’s thesis is one of them. In which he investigates how to enforce the honest behavior of parties involved in a digital interaction over the Internet. In particular, considering two emerging paradigms in this setting: Cloud computing and E-commerce.
The Human interactions often involve people who have different and sometimes contrasting interests, like buyers and sellers or consumers and providers. For what regards physical interactions, the society has developed during the years many different ways to protect users against misbehaviors. Nevertheless, when this communication happens in the digital world through the Internet, where people do not meet or even know each other, such a protection is more challenging to obtain, and additional digital tools are needed in order to defend users.
Two main security concerns that have given attention by the research community are those about the privacy and authenticity of the data stored and processed in untrusted environments. Intuitively, for privacy a Client does not want the server to learn any information about the outsourced data. For authenticity, the Client instead wants to be sure that the Cloud computed correctly on the outsourced data.vIn his thesis he focused on this second problem, advancing the study of homomorphic authenticators. In homomorphic authenticators a Client C outsources authenticated data to the Cloud. Later on, a third entity (the Verifier) can ask the Cloud to compute a function f over the Client’s outsourced data. Using a special procedure, the Cloud can provide the Verifier with an authenticator for the output of the function, which allows the Verifier to check the validity of the computation queried.
The contribution of the thesis addresses three different aspects of homomorphic authenticators: definitions, efficiency and functionalities.
First, it introduces a new security model which is stronger and easier to deal with compared with the existing one, along with two compilers which allow one to go from the old model to the new one. Second, it provides the first linearly homomorphic signature scheme whose verification keys have size sublinear in that of the outsourced dataset. Third, it formalizes the notion of homomorphic authenticators for functions which take inputs authenticated using different keys, providing concrete constructions both in the case of private and public verification.
For what regards E-commerce and, more in general, the possibility of transferring value through the Internet, this work is focused on achieving fair exchange by profiting of the Blockchain features, where with fair exchange we mean the possibility for two users to swap digital goods such that neither can cheat the other through Zero Knowledge Contingent Payments (ZKCP) protocol.
Dario Fiore, Anaïs Querol and Matteo Campanelli, researchers of the IMDEA Software Institute, have talked about the new framework they have developed, called LegoSNARK, which paper was published at the ACM Conference on Computer and Communications Security.
Dario Fiore, Associate Research Professor, started saying that "in our society we often experience a tension between the privacy of our data and the utility of its use. For example, assume that you want to rent a house and the landlord ask you to prove that your monthly income exceeds the rental fee. Now, you would not like to reveal exactly how much you earn because for example this may induce the landlord to increase the price in the future. So, how can you then make this proof and without revealing too much information. Zero-knowledge proofs are a magical cryptographic tool that allows to prove a statement about private data without revealing more information than the fact that the statement is true".
The PhD student, Anaïs Querol started showing a physical example of how it is possible to convince the landlord that you can afford the rent. "Suppose that the rent costs 4 coins and we earn 10 coins. We insert those 10 coins inside this opaque coin dispenser, so by the shape of the dispenser at least you can see that I have 3 coins. How can I prove the landlord that I have at least 1 more? It is very simple, I simply get this one out and now you can see that I have 1,2,3 and 4. So the landlord knows that I can afford the apartment, but they have no clue about our spare money". She ends up saying that this can look quite simple, but in a digital transaction when you have to convince someone on the other side of the world cool mathematical techniques come into play to make it possible!
Matteo Campanelli, post-doctoral researcher, adds that now the emerging technologies like blockchains or cryptocurrencies are pressing out to make all these systems practical. "Recently at IMDEA what we did was tackling two of the main challenges in the space. The two main challenges are one, that these things, the digital analogy of the physical world opaque coin dispensers are very complex and the other is that they are slow. In order to tackle these problems, we develop a framework called LegoSNARK. Basically, we design techniques that allow to construct these systems not in a monolithic way but more modularly. So, think of not a whole piece of clay, but made of different construction blocks of sort, and that’s why we called it LegoSNARK. The interesting thing is that this approach also gives you more efficient zero-knowledge proofs in general".
The pre-doctoral researcher of the IMDEA Software Institute, Pedro Valero, explains the work he has done recently that has taken him to Facebook.
"Technological giants generate vast amounts of information constantly and the only way they have to manage this information efficiently is by compressing it. However, they keep this information because they want to process it later, so saving the information in compressed form means that every time they want to query the information it is necessary to decompress it and perform the search on the original data. We specifically have been working with textual data. In this scenario, when compressing the file you need to find parts of the text that are repeated several times. Then the repeated text is written the first time it occurs and, for the rest of the occurrences, we simply indicate that what comes next is the fragment that appeared previously. This idea allows us to compress the file and save space but it also allows us to speed up the searches because, when we are processing the text, each time we find that what comes next has already occurred before, we can reuse the information we had already obtained when processing that same string of text. This idea is conceptually simple, but we have been among the first ones to put it into practice. We have developed an algorithm that allows us to perform these searches and really saves time.
If the file can be well compressed then the search in the compressed text without decompression can be faster than the whole process of decompressing and searching.
The problem with this approach is that not every compression algorithm works. Only a certain set of algorithms that are known as dictionary algorithms, or grammar-based, are worthwhile, and those algorithms are typically not studied within industry since they are generally slightly slower and more expensive, although they can produce good results.
The work that I have been doing with Facebook is to study this type of algorithms and find out in what context they can be used since, as usual, it is not always convenient to use them, but there are some scenarios in which it is worth to spend a little more time to compress the file in exchange for being able to search faster".
The vice-president of the Community of Madrid, Ignacio Aguado, the Regional Minister of Science, Universities and Innovation, Eduardo Sicilia, and the General Director of Research and Technological Innovation visit the IMDEA Energy Institute to learn about various initiatives against climate change. The political representatives have been received by the directors of the seven IMDEA Institutes.
During the tour through several laboratories, researchers of IMDEA Energy explained several projects in which they participate and, among other things, they highlighted that they have managed to produce kerosene from CO2, water and concentrated solar energy, which constitutes a worldwide milestone that could have important consequences both for long-distance aviation and for the naval sector.
In his speech to the media, Ignacio Aguado stated that "investing in scientific innovation and cutting-edge research programmes is a priority for this Government", which allocates 1.71% of its GDP to R&D activities.
The IMDEA Software Institute also contributes to the climate cause. Computer systems, from data processing centres to personal mobile devices such as smartphones, are major energy consumers. Reducing this consumption without cutting performance is a major challenge with a clear positive impact on the environment. Traditionally, there have been attempts to improve hardware, and currently, the focus is on improving software to perform the same functions with lower energy consumption.
View the photo gallery
Manuel Bravo, Post-doctoral Researcher at the IMDEA Software Institute has proposed elegant algorithms for transaction processing in FARM-like databases, proved their correctness and identified how they should be changed to exploit Remote Direct Memory Access (RDMA), a new networking technology that has the potential to drastically increase the scalability of distributed databases. However, to realize this potential, the algorithms for transaction processing in such databases have to be radically redesigned.
The first industrial database to use RDMA is the recent FARM system from Microsoft, which is now used to compute some of the search queries in Microsoft Bing. Unfortunately, the theoretical foundations of FARM have been shaky: its algorithms have not been proven correct and the rationale many of its design decisions was unclear.
Bravo, that has presented this proposal as a paper to PODC, demonstrates that the methodology for modifying transaction processing algorithms to run over RDMA also opens the door to exploiting RDMA for scaling up other industrial databases. This work has increased confidence in the correctness of FARM design, and allowed proposing its simplifications,
AVERTIS, an event dedicated to Analysis, Verification and Transformation for Declarative Programming and Intelligent Systems, the line of research carried out by our researcher and former director of the IMDEA Software Institute, Manuel Hermenegildo, was held last Friday, November 29th, with a large number of experts in the field.
AVERTIS became an intense and interesting day full of knowledge, scientific dissemination and companionship.
In total, the event had 13 exceptional speakers: Roberto Giacobazzi; Patrik Cousot; Andy King; María García de la Banda; David S. Warren; María Alpuente; Narciso Martí Oliet; Martin Wirsing; Veronica Dahl; Peter Stuckey; Mike Codish; Gopal Gupta; and Ricardo V. Peña Mari.
View the photo gallery.
Speculative execution attacks, such as Spectre, exploit critical vulnerabilities in modern processors to leak sensitive information. Marco Guarnieri, José F. Morales and Andrés Sánchez, from the IMDEA Software Institute, Boris Köpf, from Microsoft Research, and Jan Reineke, from Saarland University, have created Spectector, a tool for proving programs secure against such attacks. The research has been supported by a grant from the Intel Strategic Research Alliance.
Spectector implements the first principled approach for reasoning about the information leaks exploited by Spectre-style attacks. Spectector leverages symbolic execution and self-composition to automatically prove that programs satisfy a property called speculative non-interference, which guarantees the absence of speculative leaks, or detect violations.
Using Spectector, they detected subtle bugs in the way Spectre-countermeasures are placed by several major compilers, which may result in insecure programs or unnecessary countermeasures.
One of the evidences of the tool’s success is that this month the paper has been accepted at the IEEE Symposium on Security and Privacy 2020.
More than 150 high school students attended the activity "The Roots of Software", on the occasion of the Science and Innovation Week, an initiative from the Comunidad de Madrid, coordinated by the Knowledge Foundation Madri+d, aimed at introducing young talents to software research through challenges, games and videos. A different way of disseminating the science of the IMDEA Software Institute, promoting STEM vocations and attracting future promises.
The director of the Institute, Manuel Carro, was in charge of opening the event and welcoming the students. After him, a promotional video was presented. It tells in a direct and impressive way, the work that is done in software research.
Once the video broadcast was over, the pre-doctoral researchers Silvia Sebastián and Pedro Valero, began to tell what they do and quickly moved on to the games that entertained young people for more than two hours.
They taught the students how problems can be solved faster thanks to parallelization, with sums of large numbers in parallel. Several volunteers were invited to go out on the whiteboard and try to solve the equation in the shortest possible time. In addition, they explained that when working in parallel, it is necessary to coordinate the processes (concurrence). In this sense, the students successfully tried to solve the problem of the philosophers' dinner.
Cryptography was also present, Silvia and Pedro hid a report and the attendees had to break the encryption to know its location.
Another themes of the games were formal systems, the turing test to differentiate humans from machines and finally they used the Kahoot tool so that the young people could vote if the people from the images and videos that were shown to them were fruit of an artificial intelligence or human.
View the photo gallery
The Madrid high-speed network for universities and research, REDIMadrid,an iniciative from the Community of Madrid and managed by the IMDEA Software Institute, celebrates its XIV Conference next October 22nd in the Departmental II of the Móstoles Campus of the Rey Juan Carlos University (URJC).
The conference is a meeting point between research institutions and industry for the exchange of ideas and successful experiences on the application of technologies of very high-speed telematic networks.
The programme for the 2019's edition will start at 9:00 and end at 16:30.
The vice-rector of Digitalization and Internationalization of the URJC, Abraham Duarte Muñoz, will be in charge of opening the event in which there will be speakers from REDIMadrid, the URJC, the Universidad Politécnica de Madrid (UPM), UNED, ADVA Optical Networking, Axians, [Palo Alto](palo alto california) and HPE Aruba Iberia.
Blockchain is not a fad, it is a promising technology that has wide applicability. Sustainability is not only a noun; protecting our planet has become a moral obligation. This is why chainrEaction has been created. It is the first hackathon organized by the IMDEA Software Institute y EIT Digital on the use of blockchain technology to develop sustainable solutions for the communities of the future and thus slow down climate change.
ChainrEaction has two main objectives: bring students closer to research and innovation in the area of blockchain; and contribute to the creation of novel solutions for a more sustainable future.
The event will take place from the 3rd to 5th of February 2020 in Madrid, Spain. A maximum of 33 students can attend and to make sure that you can get here, we will provide travel grants. You will enjoy a unique learning and hacking experience, with a program composed of research and industry talks, technical tutorials and ample time for hacking in groups of 3. You will be guided by top researchers from the IMDEA Software Institute and other research institutions.
The key areas of chainrEaction are:
We accept applications from students in Computer Science and related fields, at the BSc, MSc and PhD level. We will select the all-round strongest candidates – blockchain experience is not a must! Applications until the 17th of November 2019 (23:59 UTC) through: https://apply.chainreaction.es/.
Carro welcomed the nearly 200 young people who attended. He introduced the crime simulation format that was going to be recreated and assured that "today there are no actors, the researchers that you will see are part of the staff of all the IMDEA Institutes and the members of the Police are not only part of the General Direction of the Scientific Police, but everything they will do at the crime scene is the same as they would do in real life". Finally, the director of the Institute ended by making the room aware that science is behind almost everything.
In this occasion the action takes place in a research center. One of its members appears dead in his office and from there the Scientific Police, as well as researchers come into action to collect and analyze evidence from the crime scene.
The researcher Matteo Campanelli talked about privacy during his presentation and how some tools that are sold as secure offer sensitive user information with which many things can be deduced, such as a person's identity. In this sense, he analyzed the Tablet of the corpse and finds an anonymized clinical database that along with other public data on the web, reveals that he had information about the pregnancy of a partner. From which it can be deduced that the victim was blackmailing her.
Once again, in the end thanks to the joint collaboration between investigators and the National Police, the victim was found guilty of the crime.
View the photo gallery.
Today marks the launch of a pilot project, OPENQKD, that will install a test quantum communication infrastructure in several European countries. The IMDEA Software Institute will participate in the recently funded EU project OPENQKD by providing physical infrastructure and the expertise of personnel of the REDIMadrid innitiative, managed by the Institute. The whole consortium is composed by 38 members, 4 of them from Spain.
Classical and quantum communications will jointly ensure the ICT needs of European governments, service industries (e.g. health, finance), businesses and citizens, even in the presence of quantum computers, or other sophisticated algorithmic attacks against public key infrastructures.
The Project mission is the establishment of QKD-based secure communication as a well-accepted, robust and reliable technology instrumental for securing traditional industries and vertical application sectors, and to prepare the deployment of Europe-wide QKD-based infrastructure in future.
The high level objetives are: raising the awareness of the maturity of QKD; working with end-users to test and validate end-to-end security for businesses and industry sectors based on QKD; advancing QKD systems and QKD-based secure-communication solutions to meet market demands in terms of specifications, standards & certification; and finaly, provide several open test facilities to encourage the development of new QKD-based applications by a wide community.
REDIMadrid is deploying a research network over its own infrastructure. The aim is to avoid a hired capacity network, with new dark-fiber laid out and used exclusively for research activities.
In this context, REDIMadrid will facilitate that quantum lambdas can coexist with lambdas of research traffic, so, it will be possible to verify how the solution works in a real environment.
To achieve its ambitious goals, the OPENQKD project will last three years and have a budget of €15 million funded under H2020-EU.2.1.1. This project has received funding from the European Union´s Horizon 2020 research and innovation programme under the grant agreement no. 857156.
View the press release.
The aerospace division of the engineering and technology group (SENER) has received today the Madrid Regional Minister of Education and Research, Mr. Rafael van Grieken, and the General Director of Research and Innovation, Mr. Alejandro Arranz, to present the company activities in the aerospace sector, especially the 'Madrid Flight on Chip' project, partially funded by the Madrid Regional Government and the European Regional Development Fund.
The General Manager of SENER Aerospace, Mr. José Julián Echevarría, and the Business Development and Strategy Manager of SENER Aerospace, Mr. Diego Rodríguez, welcomed the attendees, gave an initial presentation of the work being carried out at SENER, and briefly explained the 'Madrid Flight on Chip' (MFoC) project. Afterwards, there was a tour showcasing some of the main projects and capabilities of SENER in the aerospace sector.
The visit ended with a more in-depth presentation of the MFoC project by the representatives of the partners: SENER (project coordinator), the Carlos III University of Madrid (uc3m), the IMDEA Software Institute, The Reuse Company, Centum Solutions, Genera Tecnologías, and MARM.
The scientific director of IMDEA Software, Manuel Carro, said: "software is playing a predominant role in aerospace technology today. Moving from embedded, intercommunicating, and certified systems to having system-on-chip makes developing their software much more challenging than before". In addition, Carro has declared how important it is for the IMDEA Software Institute to participate in a project of this caliber: "we are very happy to collaborate in MFoC because it gives us exposure to a type of software - -aerospace software- to which we do not normally have access. By its characteristics, we believe it is a class of complex software that performs essential functions and that we see a an opportunity to apply and evolve our capabilities, while still posing an affordable challenge".
Rafael van Grieken, Regional Minister of Education and Research, stated that Madrid is a focus of attraction for companies today but that there is still a need to strengthen business initiatives, particularly based on advanced technologies. "I am convinced that the Madrid Flight On Chip project will impact more satellites, more companies, and many more people on planet Earth than those of us who are here in Madrid and in Spain", concluded Mr. van Grieken.
Luís Moniz Pereira, NOVA LINCS Researcher, emeritus Professor at DI FCT NOVA, and member of the Board of Trustees and the Scientific Advisory Board of the IMDEA Software Institute, received the National Science Merit Award 2019 from Portugal, on July 8.
Along his career Pereira has been, among other things, the founding president of the Portuguese Association of Artificial Inteligence becoming one of the pioneeers and most outsdanding researchers in Portugal.
The Lisbon Congress Palace hosted the Science 2019 - Science and Technology Summit in Portugalwhere the awards ceremony was held.
Lucas Kuhring and Zsolt István, researchers at the IMDEA Software Institute, will present a demo "I Can't Believe It's Not (Only) Software! Bionic Distributed Storage for Parquet Files" at the 45th International Conference on Very Large Data Bases (VLDB'19) in Los Angeles, USA.
The size of data to be stored and processed as part of data science applications is increasing and leading to bottlenecks and inefficiencies in the datacenter. A way to reduce these bottlenecks is by tailoring the underlying distributed storage solution to the application domain, using resources more efficiently. Lucas and Zsolt have explored this idea in the context of a popular column-oriented storage format used in big data workloads, namely Apache Parquet.
The prototype they have created uses a storage node based on Field Programmable Gate Arrays (FPGAs) that offers high bandwidth data deduplication and, in the future, near data processing for machine learning workloads. The hardware is combined with a software library that allows transparent access to Parquet files.
The demonstration shows that it is possible to implement in-line deduplication without increasing latencies significantly or reducing throughput by relying on the FPGA's dataflow processing model. It also highlights the benefits of implementing the application-specific aspects in a software library instead of FPGA circuits and how this enables, for instance, regular data science frameworks running in Python to access the data on the storage nodes.
Like every year, the IMDEA Software Institute publishes its annual report that summarizes in general terms the activity that has been carried out during that period of time.
2018’s edition not only updates relevant content but also design and structure. These efforts have been made to make the document more visual, compelling and easier to read.
Last year the Institute was composed by 62 researchers from 18 different nationalities, of which, 26 were PhD students.
Madrid Flight on Chip', 'Verification with Liquid Types' and 'Narrowing the data/Compute Gap with Specialized Hardware' are the three research highlights in this report. It also includes the research projects and contracts in which the Institute has been working during 2018 and those that have begun this year.
For more information, please consult the 2018 annual report link to publication.
The pre-doctoral researcher of the IMDEA Software Institute, Pepe Vila, was one of the speakers at RootedCON 2019, which took place from March 28 to 30, in Madrid. More than 2,500 people attended the event born with the purpose of promoting the exchange of knowledge among members of the security community.
You can view the full presentation (in Spanish) here
The Madrid Science and Innovation Fair (MXCI) 2019, organised by the Madri+d Knowledge Foundation and IFEMA, in connection with the #STEMadrid initiative, concludes after four intense days and a large number of visitors. The IMDEA Institutes had the privilege of being there with a stand representing four Institutes (networks, energy, nanoscience y materials) on Thursday and Friday, nd three Institutes software, water y food) on Saturday and Sunday.
This days were full of interesting activities dedicated to show visitors the research done by the Institutes as part of an initiative to promote the excellence in science in the Community of Madrid.
The presence of IMDEA Software at the Fair was a great opportunity to disseminate the research being carried out at the Institute, demystify computer science and encourage STEM vocations. More tan four activities were carried out that helped visitors, in a pleasant and attractive way, to understand what software is, how it works internally and where it is located. In this way, as much information as possible was provided for those who had an interest to awaken a vocation and become great talents in the future.
In particular, on Saturday afternoon, the Institutes IMDEA Software and IMDEA Food collaborated with the Spanish National Police to carry out an activity focused on publicizing "The Science that Investigates Crime". Some visitors were able to put themselves in the shoes of the National Police and helped them gathering evidence from the crime scene. These evidence was then given to the researchers that explained how they are able to extract important information that can help the Police solving the crime.
IMDEA Software IMDEA Software Institute Faculty Zsolt István was awarded a Marie Skłodowska-Curie Individual Fellowship, for the Project Accelerated Ordering Service for Distributed Ledgers (ACCORD). The project sets out to improve blockchain systems that target Business to Business use-cases and builds on earlier success in the use of specialized hardware to implement distributed algorithms.
Distributed ledgers (DLs), or blockchains, have the potential of transforming the ways individuals and businesses interact by reducing the cost of transactions and the associated delays dramatically. How can this be done? Delegating today’s trusted third party guarantee to a distributed computing network that relies on cryptographic operations and sophisticated distributed consensus algorithms to ensure that transactions are recorded durably and in a tamper-free manner.
The adoption of DLs outside of crypto-currency use cases has been slow for performance reasons. The ACCORD project aims to increase distributed ledger throughput by at least an order of magnitude, while lowering latencies by a similar factor. To achieve this, the focus is on the core component of DL systems, namely, distributed consensus that is used to establish an absolute order of transactions. This ordering operation is one of the main performance bottlenecks in DLs. So, to fully exploit emerging network technologies and to overcome stagnating CPU performance, ACCORD is planning to use hardware acceleration to offload the steps required by the ordering service.
In the end, the foreseen outcome of the ACCORD project is a DL design with performance that allows it to be deployed in use-cases in which DLs are inadequate today as, for example, trading.
This project has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No. 842956.
Next February 11, on the occasion of the International Day of Women and Girls in Science, the Montegancedo Campus will host the conference "I+D+M². Women in Montegancedo" organized jointly by the Universidad Politécnica de Madrid, through the Cajal Blue Brain Project and the Ontology Engineering Group, and the IMDEA Software Imstitute. This is a great opportunity to bring science and research closer to girls and adolescents, to encourage STEM vocations and to interact with young researchers as well as with those who have a consecrated career.
Those attending the conference will have the opportunity to meet women researchers with a consolidated career, the research carried out on campus and will discuss the role of women in science. It is undoubtedly a suitable event to resolve all the concerns that arise when deciding on the academic future.
The aim of this conference is to promote the participation of more women in Science, to highlight the difficulties they encounter during their professional careers and to encourage young researchers to start or continue with their scientific careers.
The meeting will take place from 9:00 a.m. to 5:30 p.m. in the auditorium of the Business Centre of the Montegancedo Campus. Attendance at the event is free but registration is required here.
The IMDEA Software Institute, the Universidad Complutense de Madrid (UCM) y la Universidad Politécnica de Madrid (UPM), have been beneficiaries of the Call for R&D Program Activities of the Comunidad de Madrid, thanks to the project "Intelligent Contracts and Scalable Blockchains and Insurance through Verification and Analysis" (BLOQUES-CM), which has a financing of 763,600 euros, by the Comunidad de Madrid with the support of the European Union Structural Investment Funds.
The Research Group aim to address major challenges of systems based on blockchains and smart contracts, which must be solved so that its use is reliable in areas where high levels of security and data integrity can be achieved.
BLOQUES-CM will advance in the state of: the properties of integrity and anonymity, the verification of infrastructures, the testing of blockchains and, in the tests of correction and use of resources.
In this sense, BLOQUES-CM, among other thing, aims to prevent disappearances or the acceptance of incorrect transactions.
Roberto Giacobazzi, affiliate faculty at the IMDEA Software Institute, received a Distinguished Paper award at the flagship conference of Principles of Programming Languages POPL’19, in Cascais, Portugal, for his work, coauthored with Francesco Ranzato, from the University of Padova, and Patrick Cousot, “A²I: Abstract² Interpretation”.
Their article formalizes offline and online meta-abstract interpretation and illustrate this notion with the design of widenings and the decomposition of relational abstract domains to speed-up program analyses. This shows how novel static analyses can be extracted as meta-abstract interpretations to design efficient and precise program analysis algorithms.
In total, three papers by researchers from the IMDEA Software Institute were accepted at POPL’19, supporting once more the high quality of the research performed at the Institute.
The director of IMDEA Software Institute, Manuel Carro @manuel__carro, will be part of the third round table of the event "Innovation and R & D in Emerging Technologies for Digital Transformation", based on research and innovation in Madrid, which is organized by the Information Processing and Telecommunication Center (IPTC) in the ETSI Telecomunicación of the UPM on January 15, 2019.
This event arises with the purpose of reflecting and analyzing the existing models of development and technological, economic and social relationship between the different agents involved in the processes of digital transformation and the progress of key technologies such as: Cloud, IoT, AI, 5G, Big Data and Cybersecurity.
In addition to IMDEA Software Institute, representatives of companies such as NTT Data,Amazon or Santander; industrial associations such as Madrid Foro Empresarial or DigitalES; representatives of national and regional R & D management entities; and experts from the academy belonging to different Technology Centers, such as IMDEA Materials and the Industrial Electronics Center.
Free entry until complete seats. Registration and more information here.
UPM's 6th Technology Innovation workshop took place at the IMDEA Software Institute. As part of its commitment to empower technology advance and innovation, the IMDEA Software Institute collaborated in the organization of UPM's yearly workshop. The workshop feature keynote speakers and a showcase of some of the best ideas presented to the Innovatech Challenge, as well as the award ceremony for the winners of the contest of ideas.
EIT Digital Spain held its Innovation day 2018, with the participation of several keynote speakers and panelists. Manuel Carro, the director of the IMDEA Software Institute, gave a short presentation on innovation from the perspective of a research center: what innovation is and how higher education can be taken advantage of by research centers and the industrial ecosystem to foster innovation.
The Minister of Science, Technology, and Higher Education of Portugal, Mr. Manuel Heitor, visited the IMDEA Software Institute and the EIT Digital Spain node, together with Mr. Raul Azevedo, director of the recently created DTX Digital Transformation CoLab.
Mr. Heitor and Mr. Azevedo discussed potential lines of collaboration between different stakeholders in Portugal and the IMDEA Software Institute and EIT Digital with Manuel Carro and Jesús Contreras, directors of the IMDEA Software Institute and the EIT Digital Spanish node.
Miriam García (now at IST Austria), a former PhD student at the IMDEA Software Institute under the supervision of Pavithra Prabhakar (now at Kansas State University), has been awarded one of the 2016/17 UPM PhD thesis prizes.
There were a total of three awards for thesis defended at the Computer Science School.
IMDEA researcher Zsolt István is one of the ETH Outstanding Doctoral Theses 2018 Award Winners for his PhD Thesis: “Building Distributed Storage with Specialized Hardware”. (Department of Computer Science Award Winners).
IMDEA Software Institute researcher Niki Vazou has been awarded a distinguished paper award at the ACM Sigplan conference Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA) 2018 for the paper “Gradual Liquid Type Inference". The conference awarded 4 distinguished paper awards among 59 accepted papers.
The paper is a collaboration with Éric Tanter (University of Chile) and David Van Horn (University of Maryland) and combines gradual with liquid types to aid program migration and provide better error messages.
EIT Digital, the European KIC on Information Technologies, organized an event on Digital Finance. The event, held at the Co-Location Center of the Madrid Node of EIT Digital, hosted at the IMDEA Software Institute, featured a round table on business financing through Open Banking and talks by invited speakers. In particular, Atos presented OFION, an initiative nurtured under the umbrella of a innovation and transference activity partially funded by EIT Digital that offers a technological solution to implement flexible invoice factoring in SMEs.
IMDEA Software Institute student Platon Kotzias and researcher Juan Caballero have been awarded a distinguished paper award at the SIGCOMM Internet Measurement Conference (IMC) 2018 for the paper “Coming of Age: A Longitudinal Study of TLS Deployment”. The conference awarded 3 distinguished paper awards among 43 accepted papers out of 174 paper submissions.
The paper is a collaboration with researchers Abbas Razaghpanah (Stony Brook University), Johanna Amann (ICSI/Corelight/LBNL), Kenneth G. Paterson (Royal Holloway, University of London), and Narseo Vallina-Rodriguez (IMDEA Networks / International Computer Science Institute).
Lambda World is a conference aiming to scale the usage of the research achievements in the area of functional programming over the last 40 years in the industrial setting. Aleks Nanevski and Anton Trunov have tried to push it even further, showcasing modern technology, like proof assistants, built on top of dependent types. This approach is highly desirable in the branches of industry needing high assurance guarantees. Anton delivered a workshop on programming in Coq aiming at software developers. And Aleks presented a talk on proof automation using Coq’s canonical structures.
Manuel Carro, director of the IMDEA Software Institute, will be interviewed in the Spanish National Radio (RNE) program “Por tres razones” (For Three Reasons) on Friday, September 28th.
The program runs from 19:00 to 19:45, and will be made available on the website of the program.
Researchers from other IMDEA Institutes and the Director General for Universities of the Comunidad de Madrid will take part in the program as well.
The IMDEA Software institute hosted the third International Workshop on Dynamic Software Documentation (DySDoc3), and the pre-reception of the 34th International Conference on Software Maintenance and Evolution (ICSME) with talks by Bitergia, CQSE and Sourced.
Manuel Carro, the director of the IMDEA Software Institute, contributed again to the Spanish podcast “1BIT de memoria”, focused on the life and achievements of great computer scientists, specifically Turing prize award recipients.
This time, the podcast focused on Leslie Lamport, widely known for his contributions to concurrent and distributed systems, verification, and for being the creator of LaTeX, one of the systems for document preparation most widely used in scientific and technical environments.
IMDEA Software Institute researcher Alexey Gotsman, along with Gregory Chockler (Royal Holloway, University of London), has received a best paper award at the International Symposium on Distributed Computing (DISC 2018). The award was given for the paper “Multi-shot distributed transaction commit”.
IMDEA Software Institute PhD student Pepe Vila discovered a vulnerability in Google Chrome (CVE-2018-16075) that allowed any local HTML file to steal cookies and content from arbitrary domains. This issue has been patched in version 69.
IMDEA Software Institute researchers have presented several papers at the 34th International Conference on Logic Programming (ICLP'18), that this year was a part of the Federated Logic Conference (FLoC'18), held July 14-17, 2018, in Oxford, UK. FLoC is a major event celebrated once every four years which gathers all the major conferences related to logic and computer science. ICLP is the top international venue in the area of Logic Programming and is part of FLoC.
IMDEA Software Institute director Manuel Carro was a member of the Program Committee of ICLP this year. PhD student Joaquin Arias presented s(CASP), a system developed in collaboration with Manuel Carro and researchers from the University of Texas at Dallas. s(CASP) evaluates non-monotonic programs with constraints avoiding the combinatorial explosion due to the grounding phase. The paper entitled "Constraint Answer Set Programming without Grounding", to be published in Theory and Practice of Logic Programming, describes this novel execution model and shows through several examples the enhanced expressiveness of s(CASP) w.r.t. ASP, CLP, and other CASP systems.
PhD student Maximiliano Klemen presented a technical communication on his work with recent PhD graduate Nataliia Stulova, and IMDEA Software faculty members Jose F. Morales, Pedro Lopez-Garcia, and Manuel Hermenegildo, entitled "Towards Static Performance Guarantees for Programs with Run-time Checks". This work presents a framework for reasoning statically about the overhead added to programs by run-time checks in terms of both algorithmic complexity and actual cost changes. Moreover, the framework allows programmers to specify an "admissible" overhead level per program routine (function, predicate, etc.), and automatically and statically check whether the program with run-time checks adheres to such specification for all possible executions.
PhD student Isabel Garcia presented a technical communication on her work with IMDEA Software faculty members Jose F. Morales and Manuel Hermenegildo, entitled "Towards Incremental and Modular Context-sensitive Analysis". This work tackles the issue of the high cost of context-sensitive static analysis on large code bases during the development process. The authors present an approach that combines fine-grain incrementality and modularity, which was not covered by previous approaches. Analysis results are updated at the particular places where the changes to the code are introduced (incrementality), which is significantly less costly than performing global system-level analysis. Local updates are propagated as necessary to the affected program units (modularity), obtaining the same results as standard modular global analysis with greatly reduced cost.
Faculty member Pedro Lopez-Garcia presented his work with PhD student Maximiliano Klemen, recent PhD graduate Umer Liqat, and faculty member Manuel Hermenegildo, entitled "A General Equational Framework for Static Profiling of Parametric Resource Usage" at the 19th Workshop on Logic and Computational Complexity (LCC'18). This novel framework for setting up cost relations can be instantiated for performing a wide range of resource usage analyses, including both static profiling of accumulated cost and the inference of standard notions of cost. This allows identifying statically the parts of programs that have the greatest impact on the total cost.
The IMDEA Software Institute has published its 2017 Annual Report.
Leaving their usual attachment to well-proven technologies and procedures, banking is embracing AI at all levels, from the interaction with clients to their core business.
This trend opens new problems and opportunities in a very powerful sector extremely relevant for our everyday life.
Not only that: the future relationship of banking and AI can shape the role of banking in the society, and how banking deploys their internal processes.
This was the main topic of a panel held on June 22, 2018, by the El Español digital newspaper.
In this meeting, several experts, namely Miquel Moya (Google), Javier Gonzalez Dominguez (Digital Innovation and Big Data, Evo Banco), Rodrigo Miranda (ISDI), Javier Iglesias (Salesforce Iberia), Manuel Carro (UPM and IMDEA Software), and Giorgio Semenzato (Finizens), exchanged their opinions on the solutions that AI can bring to baking and the challenges that this adoption can bring about.
An innovative application of AI in the form of a voice-driven interface adopted by EVO Banco was used to showcase possible application fields.
Former IMDEA Software Institute intern Anaïs Querol Cruz has been selected as a recipient of a prestigious fellowship from “La Caixa” Foundation to carry out a PhD at our Institute. This was the outcome of a competitive selection process that awarded only 20 fellowships out of 602 evaluated applications.
More information here
IMDEA Software Institute recent PhD graduate Luca Nizzardo gave an invited talk at an event on blockchain and cryto values organized by Codemotion in Milan, Italy. The title of Luca's talk was “Bitcoin and Beyond(?), a Cryptographic point of view”.
IMDEA Software Institute faculty member Dario Fiore, together with postdoctoral researchers Antonio Faonio and Matteo Campanelli and other members of the Spanish cryptography community, participated in the presentation ceremony of the 10th BBVA Foundation Frontiers of Knowledge Awards. The ceremony was held at the Marqués de Salamanca Palace of Madrid.
This year the BBVA Foundation gave fourteen awards covering eight categories: basic sciences, biomedicine, climate change, ecology and conservation biology, information and communication technologies, economics finance and management, development cooperation, and contemporary music.
This year's award in the information and communication technologies category is specially relevant for the IMDEA Software Institute. It was given to professors Shafi Goldwasser, Silvio Micali, and Ronald Rivest from the MIT, and to professor Adi Shamir from the Weizmann Institute of Science for their “fundamental contributions to modern cryptology, an area of a tremendous impact on our everyday life”. Cryptography is one of the strongest areas of the IMDEA Software Institute, and we want to take this occasion to warmheartedly congratulate these four outstanding scientists for their achievements and well-deserved recognition.
IMDEA Software Institute researcher and deputy director Juan Caballero gives an invited talk at the 1st OPTICS2 Workshop on Avionics Cybersecurity on June 5-6 in Cologne, Germany. The workshop was organized by the European project OPTICS2. Juan delivered a talk on the evolution of malware network communications titled “A Lustrum of Malware Network Communication: Evolution and Insights”.
PhD students Nataliia Stulova and Luca Nizzardo successfully defended their PhD theses. On May 23, Nataliia defended her thesis entitled “Improving Run-time Checking in Dynamic Programming Languages” and advised by IMDEA researchers José Francisco Morales and Manuel Hermenegildo. On May 24, Luca defended his thesis entitled “Cryptographic Techniques for the Security of Cloud and Blockchain Systems” advised by IMDEA researcher Dario Fiore.
Both Nataliia and Luca obtained their degree from the Technical U. of Madrid (UPM) within the DSS doctoral program, in which IMDEA faculty collaborate.
Pictures of the defense of Nataliia and Luca:
The Tezos Foundation is establishing a multi-year research, training, and dissemination program with IMDEA Software Institute to address Tezos-related technologies including cryptography, computer security, formal verification, distributed systems, and programming languages.
IMDEA's program will focus on the technology surrounding the Tezos cryptographic ledger and smart contracts, which will help advance developments in privacy, correctness, robustness, and scalability. The Tezos Foundation will also offer support to IMDEA's successful Master's/PhD program with the Technical University of Madrid to provide additional focus and research on topics related to Tezos.
The team of the MATHADOR project (led by Aleks Nanevski) is pleased to announce the first release of the FCSL-PCM library. FCSL-PCM is a part of Fine-grained Concurrent Separation Logic framework, more information is available at https://software.imdea.org/fcsl/. The source code can be found at https://github.com/imdea-software/fcsl-pcm.
The student Matías Spatz from the German School has joined the IMDEA Software Institute for an educational stay for a period of two weeks. Matias will be supervised by Dr. Juan Caballero who works on the area of cybersecurity.
IMDEA Software collaborates with the German School in its educational stay program for secondary school students. The goal of these educational stays is for students to learn first hand how a company or research center works, as well as their techniques and working approach. These stays at the IMDEA Software Institute will provide a practical complement to the studies, offer a view of the life of a researcher in computer science, ease the integration into the job market, and help to disseminate science among young students.
IMDEA Software Institute researcher Pierre Ganty was invited speaker at the International Workshop on Synthesis of Complex Parameters part of the European Joint Conferences on Theory and Practice of Software.
IMDEA Software Institute Phd student Luca Nizzardo was a panel member for an event on crytocurrencies organized at the University of Milano Bicocca. He served on the panel as an expert on the crytographic aspects of cryptocurrencies.
Next Wednesday, February 7 at 16:00, a round table will be held in the IMDEA Software Institute's auditorium to contribute to the International Day of the Woman and the Girl in Science. This event is celebrated around the world on February 11 and its goal is to achieve full and equal participation in science for women and girls. The round table, moderated by journalist María José Bosch, will be recorded live, and it will be broadcast on Friday, February 9, in the second part of Gestiona Radio's program "Primera Hora" (from 11:00 to 12:00).
Two researchers from IMDEA Software (Alessandra Gorla and Isabel García Contreras) and three invited professors and researchers from other institutions will participate: Ernestina Menasalvas, professor at E.T.S. of Computer Engineers of the UPM; Asunción Santamaría, professor at the E.T.S. of Telecommunication Engineers of the same University; and Elena González-Blanco, General Manager for Europe at CoverWallet and Principal Investigator of the POSTDATA ERC project.
With this round table, open to the public, IMDEA Software joins similar activities organized by the seven IMDEA Institutes with the support of the MadrI+D Foundation and the Ministry of Education and Research of the Community of Madrid.
Links of interests:
Manuel Hermenegildo, Distinguished Professor at the IMDEA Software Institute, has been appointed Chairman of the Scientific Board of INRIA, the French Institute for Research in Computer Science and Automation (Institut national de recherche en informatique et en automatique). He succeeds Professor Kurt Mehlhorn, director at the Max Planck Institute for Informatics, who held the position from 2015.
INRIA is a French national public research institution focusing on computer science and applied mathematics. It comprises 8 research centers (in Bordeaux, Grenoble-Inovallée, Lille, Nancy, Paris-Rocquencourt, Rennes, Saclay, and Sophia Antipolis) and employs 3800 people, including 1300 researchers, 1000 Ph.D. students, and 500 postdocs.
The INRIA Scientific Board provides guidance on the major aspects of INRIA's scientific policy, including the development of the research centers and teams, and the appointment and renewal of directors, in agreement with the Board of Directors.
Professor Roberto Giacobazzi of the University of Verona, Italy and IMDEA Software Institute visiting faculty member is hosting a Shonan Meeting on Intensional and extensional aspects of computation: From computability and complexity to program analysis and security. The meeting takes place at the Shonan Village Center, Japan, January 22–25.
Professor Roberto Giacobazzi of the University of Verona, Italy and IMDEA Software Institute visiting faculty member gives a tutorial on Code Obfuscation at the Tutorial Fest of the ACM Symposium on Principles of Programming Languages (POPL), a flagship conference in this area.
Former PhD student Goran Doychev receives the “Premio Extraordinario de Tesis Doctorales” de la ETS de Ingenieros Informaticos from the Technical University of Madrid (UPM), Spain for the 2015‐2016 course.
Goran's thesis "Tools for the Evaluation and Choice of Countermeasures against Side-Channel Attacks" was supervised by IMDEA Software Institute faculty member Boris Köpf. His thesis focuses on the development of tools to support designers and implementers at the time of choosing the best countermeasures to avoid information leakage through side channels during the execution of cryptographic protocols.
The Spanish speaking podcast “1BIT of memoria” featured IMDEA software researcher Juan José Moreno as their main guest.
Link to the podcast episode.
IMDEA Software Institute researcher Dario Fiore gives a keynote at the Nordic Conference on Secure IT Systems NordSec2017 who took place November 8-10 in Tartu, Estonia. Dario delivered a keynote entitled “Homomorphic Authentication for Computing Securely on Untrusted Machines”.
Professor Roberto Giacobazzi of the University of Verona, Italy and IMDEA Software Institute visiting faculty member gave a talk at the Fall Days on System and Software Analysis held in Nunspeet, the Netherlands, November 6-10.
Roberto's talk is entitled “Securing Code — Hacking the precision of program analysis” and concerns the design of code protecting transformations for anti reverse engineering applications.
In their opening episode, the spanish speaking podcast “1BIT of memoria” featured IMDEA software director Manuel Carro as their main guest.
Link to the podcast episode.
Juan Caballero, Associate Research Professor & Deputy Director at the IMDEA Software Institute, gave an invited talk at Cybersecurity with the Best, the World's biggest cybersecurity online conference for developers. Cybersecurity with the Best was held online on October 14-15, 2017. It comprised of over 40 talks by renowned international cybersecurity experts. Dr. Caballero's talk was titled "The Rise of Potentially Unwanted Programs: Measuring its Prevalence, Distribution through Pay-per-Install Services, and Economics" and it described recent research performed by his group at the IMDEA Software Institute, in collaboration with Symantec Research, on potentially unwanted programs (PUP), a class of undesirable programs that affects a large number of Internet users.
IMDEA researcher John Gallagher will be the program chair of the following events.
The European Researchers' Night and the related activities to be developed in Madrid were the main topics of the interview done to Manuel Carro, professor at the Technical University of Madrid (UPM), Spain, and director of the IMDEA Software Institute by the National TV program La Tarde en 24 Horas. Many research institutions and universities based on the Madrid region will bring researchers and their work closer to the society through almost 40 activities coordinated by the Fundación para el Conocimiento madrimasd next September 29th.
The seven IMDEA Institutes of the Madrid region will jointly present, with the support of the National Police, how science and technology help solving a crime and finding the criminal and its motivation. All of this will take place at the Residencia de Estudiantes on Friday September 29th, from 6pm to 9pm.
Researcher Carolina Inés Dania and Marina Egea (Minsait (by Indra)) win 2017 Best Paper Award for the article "SQL-PL4OCL: An automatic Code Generator from OCL to SQL Procedural Language” published in the Journal of Software and Systems Modeling and presented at the conference MoDELS 2017, Austin, Texas, USA.
The paper, available here, introduces a SQL-PL code generator for OCL expressions that, in contrast to other proposals, is able to map OCL iterate and iterator expressions thanks to our use of stored procedures. Moreover, the proposed mapping can target several relational database management systems.
This edition of MoDELS took place in Austin, Texas, United States from August 28 - September 1, 2017.
Roberto Costumero, student at the Software, Systems and Computation PhD. program, has successfully presented his PhD. Thesis entitled “Big Medical Text Analytics: Querying, Searching and Understanding Clinical Data” to the committee last Wednesday 20th, September. Although Roberto’s research has not been directly performed as a member of IMDEA, he has been also giving shape to the industrial part of his thesis as he is also a member of our community in EIT Digital CLC as a student of the Doctoral School, being the first student in Madrid node to be earning his PhD. Roberto has just started his Business Development Experience for 6 months at Sanitas, in which he will be able to deliver the background of his thesis to the industry.
The Board of Trustees of IMDEA Software Institute has appointed Juan Caballero as new Deputy Director of the Institute. Dr. Caballero obtained his Ph.D from Carnegie Mellon University (USA) in 2010. He joined IMDEA Software as an Assistant Research Professor in November 2010 and was promoted to Associate Research Professor on December 2016.
The IMDEA Institutes participated in the radio show Primera Hora, hosted by Javier García Mateo in Gestiona Radio. During one hour, they spoke about science in general and, in particular, about the science they will show in an upcoming event in CSIC's Residencia de Estudiantes on the evening of September 29th. On that date, and together with members of the National Police, they will present "IMDEA-CSI: crime scene investigation", one of the activities to take place in Madrid as part of the European Researchers' Night in Madrid 2017, coordinated by the Foundation for Knowledge madrimasd.
The members of the IMDEA Institutes who participated were Juan Manuel Ortiz, from IMDEA Water; Ana Ramírez de Molina, from IMDEA Food; Rebeca Marcilla, from IMDEA Energy; Juan José Vilatela, from IMDEA Materials; Álvaro Somoza, from IMDEA Nanoscience; Antonio Fernández Anta, from IMDEA Networks; and Juan Caballero and Manuel Carro, from IMDEA Software.
A recording of the program can be found here.
Boris Köpf, researcher at the IMDEA Software Institute, has participated in the paner entitled "Formal Methods for Reliable Software Security" at the final event of the DFG priority program Reliably Secure Software Systems (RS3) that has taken place in Darmstadt, Germany, from the 4 to the 6 of September.
Alessandra Gorla, researcher at the IMDEA Software Institute, has been invited speaker at the 2nd International Workshop on App Market Analytics celebrated in Paderborn, Germany, on the 5th of September. Alessandra's talk, entitled "Mining the Google Play for Anomalies" presented several analysis techniques to identify anomalous Android applications, such as anomalies that involve mismatches between the description and the implementation, anomalies in the use of sensitive information, and anomalies in the user interface.
Researchers of the IMDEA Software Institute have given several talks at the 33rd International Conference on Logic Programming (ICLP'17), that was co-located with the 23rd International Conference on Principles and Practice of Constraint Programming (CP'17), and the 20th International Conference on Theory and Applications of Satisfiability Testing (SAT'17), held on August 28 - September 1, 2017, in Melbourne, Australia. ICLP is the top international venue in the area of Logic Programming.
Manuel Hermenegildo gave, jointly with Pascal Van Hentenryck, a plenary ICLP/CP/SAT talk dedicated to the work of Alain Colmerauer, the creator of the Prolog programming language and one of the founders of the field of constraint programming, who passed away this spring.
Nataliia Stulova presented at ICLP'17 her joint paper with José Francisco Morales y Manuel Hermenegildo entitled "Towards Run-time Checks Simplification via Term Hiding", that presents a novel approach for reducing the overhead of some run-time verification techniques by several orders of magnitude based on considering the term visibility rules prior to instrumenting a program with run-time checks.
The 15th International Colloquium on Implementation of Constraint and LOgic Programming Systems (CICLOPS'17), also co-located with ICLP/CP/SAT, was co-organized by Nataliia Stulova y José Francisco Morales, who also chaired it.
Nataliia Stulova also presented a description of her dissertation research entitled "On Improving Run-time Checking in Dynamic Languages" at the ICLP/CP/SAT Doctoral Program that will be published in the ICLP'17 Technical Communications OASIcs series (volume 58), published by Dagstuhl.
Finally, and as reported in separate news, Pedro López-Garcíagave an invited talk at CICLOPS'17 and Pedro López-García and Manuel Hermenegildogave an invited talk at ICLP'17, on occasion of the 10 year Test of Time Award received for their paper entitled "User-Definable Resource Bounds Analysis for Logic Programs".
IMDEA Software Institute's faculty members Pedro López-García and Manuel Hermenegildo have given a plenary invited talk at the 33rd International Conference on Logic Programming (ICLP'17, the premier conference in the area) on their paper "User-Definable Resource Bounds Analysis for Logic Programs", which received the "Test of Time" award as a recognition of the paper published 10 years ago that has had the largest impact. The talk described the contributions of the paper, its applications, and how it has been improved, extended, and generalized over the last 10 years, as well as a summary of its impact in other work.
IMDEA Software Institute faculty member Pedro López-García gave an invited talk on August 28 at the 15th International Colloquium on Implementation of Constraint and LOgic Programming Systems, CICLOPS'17, in Melbourne, Australia, as part of the joint international top conferences ICLP'17, CP'17, and SAT'17.
Pedro's talk, entitled "Static Profiling of Parametric Resource Usage as a Valuable Aid for Hot-spot Detection," presents a novel technique that allows performing better software optimizations, and in a more efficient way, than the ones obtained with current cost analysis tools.
IMDEA Software Institute researcher Boris Köpf, has chaired the Program Committee of the 30th IEEE Computer Security Foundations Symposium (CSF 2017) together with Steve Chong from Harvard University.
The selected program can be found here. The conference was held August 21-25, 2017 in Santa Barbara, CA, USA. The Computer Security Foundations Symposium is an annual conference for researchers in computer security. CSF seeks contributions on foundational aspects of computer security as well as their application to practice.
PhD student Pepe Vila and researcher Boris Köpf received a distinguished paper award at the 2017 USENIX Security Symposium, one of the top 4 conferences in the area, for their research paper entitled “Loophole: Timing Attacks on Shared Event Loops in Chrome”.
IMDEA Software Institute Researcher, Manuel Hermenegildo, co-organizes and chairs the 4th Workshop on Horn Clauses for Verification and Synthesis (HCVS 2017). The workshop is held on August 7, 2017 in Gothenburg, Sweden, as a satellite workshop of the International Conference on Automated Deduction, CADE 2017.
This series of workshops focuses on Horn clause-based analysis, verification, and synthesis, bringing together researchers working in the communities of Program Verification (e.g., CAV, TACAS, and VMCAI), Constraint/Logic Programming (e.g., ICLP and CP), and Automated Deduction (e.g., CADE).
PhD students Miriam García y Germán Delbianco graduated during the past month. Both students obtained their degree from the Technical U. of Madrid (UPM) within the DSS doctoral program, in which IMDEA faculty collaborate.
Miriam defended her thesis "An Algorithmic Approach for Stability Verification of Hybrid Systems", advised by the former IMDEA researcher Pavithra Prabhakar. This work proposes a novel algorithmic approach to stability verification of hybrid systems, which uses formal methods.
Germán's thesis "Tools for the Evaluation and Choice of Countermeasures against Side-Channel Attacks", was supervised by IMDEA Software Institute researcher Aleks Nanevski. The main goal of the thesis is the development and application of program logics aimed at the modular verification of stateful programs with higher-order control effects.
IMDEA Software Institute Researchers Gilles Barthe and Manuel Hermenegildo participanted in the Dagstuhl Seminar on Resource Bound Analysis, held in Schloss Dagstuhl, Germany, July 16-21, 2017. This meeting brought together the main researchers in the areas of symbolic bound analysis and worst-case execution time (WCET) analysis to discuss the state of the art and future research directions in this important area: the quality of software crucially depends on the amount of resources – such as time, memory, or energy – that are required for its execution. Understanding and bounding resource usage is not only crucial for writing efficient software but also to ensure correctness and safety of software systems, as well as their resilience to attack. Manuel Hermenegildo, jointly with Pedro López-García, Maximiliano Klemen, and Umer Liqat gave a tutorial on Cost Analysis with Recurrence Relations (using CiaoPP) and its Applications and presented their recent work on Energy Consumption Analysis and Verification, also using their CiaoPP tool. The group of Gilles Barthe presented their recent work on Relational Cost Analysis (with Ezgi Cicek, Marco Gaboardi, Deepak Garg, and Jan Hoffmann).
IMDEA Software Institute researcher Juan Caballero, graduated Ph.D. student Antonio Nappa, and former intern M. Zubair Rafique have received the Most Influential DIMVA paper 2009-2013 Award for their paper "Driving in the Cloud: An Analysis of Drive-by Download Operations and Abuse Reporting". The award recognizes the most influential paper published in a period of 5 years at DIMVA, the International Conference on Detection of Intrusions and Malware & Vulnerability Assessment. The authors received their award at the gala dinner of DIMVA 2017, which was held on July 6-7 2017 in Bonn, Germany.
The winning paper was published in DIMVA 2013. It proposed a technique to identify exploit servers managed by the same organization. Exploit servers are Web servers that try to exploit vulnerabilities in the browser and browser plugins (e.g., PDF or Flash players) of visitors. If exploitation is successful, malware is installed on the visitor's computer. This process is known as a drive-by download. In the drive-by ecosystem many exploit servers run the same exploit kit software and it is a challenge understanding whether the exploit server is part of a larger operation. The paper results revealed that although individual exploit servers have a short median lifetime of a few hours, attackers were able to sustain long-lived malware distribution by turning to the cloud, hosting their exploit servers in specialized cloud hosting services.
As a result of the paper the authors released the Malicia dataset, which comprised 11688 malware binaries collected from 500 drive-by download servers over a period of 11 months, a database that details when and from where the malware was collected, and the malware classification into families. The dataset enables, among other applications, evaluating malware clustering and labeling approaches. Since its release, the Malicia dataset has been requested by 73 research institutions worlwide.
IMDEA Software Institute researcher Dario Fiore gives an invited talk at the MathCrypt event part of the NIMS Hot Topics Workshop that took place in Daejon, Korea, 29-30 June. Dario's talk, entitled “Computing on Encrypted Data”, presents his work about how to secure computations performed remotely on data stored at an untrusted server. More information about this line of research on Dario's website.
IMDEA Software Institute researcher Carmela Troncoso has participated in the ISSS EU-Datenschutzgrundverordnung und nues CH-DSG organized by the Information Security Society Switzerland in Zurich, Suiza. Her talk, entitled “Systematic Privacy by Design engineering.” explained how to tackle the system engineering problem from a privacy point of view, describing means to reason about embedding strong privacy guarantees into ICT systems, and means to approach the evaluation of private information leakage in such scenarios.
IMDEA Software Institute faculty members Pedro López-García and Manuel Hermenegildo are, with co-authors Jorge Navas (SRI) and Edison Mera (PDC), the recipients of the 10 year Test of Time Award at the 33rd International Conference on Logic Programming (ICLP 2017), the premier conference in the area, for their paper "User-Definable Resource Bounds Analysis for Logic Programs", published in ICLP 2007. The 10 year Test of Time Award recognizes the paper published 10 years ago which has had the largest impact.
The winning paper by Navas, Mera, López-García, and Hermenegildo proposed and developed a technique that allows programmers to implement analysis and verification tools for a very wide class of resources (including execution time, energy consumption, and other user-defined quantitative properties) in a straightforward way, by just defining these resources and other parameters through simple program annotations. The program together with these annotations and resource specifications constitute the input to a customizable analyzer (implemented within the CiaoPP tool) which automatically, and without running the program, predicts the usage of the resources defined in order to guarantee that the program's resource usage will be within the specified limits.
Since its proposal in 2007 the approach and its implementation in CiaoPP have been applied by different groups for computing upper and lower bound functions on resources such as memory consumption, execution time, or energy, for a wide variety of programming languages, ranging from high-level source to bytecode and to machine code. It has also been improved, extended, and generalized in several ways over the last 10 years.
Faculty member Juan Caballero and Ph.D.student Platon Kotzias Platon Kotzias have a paper at the 36th IEEE Symposium on Security and Privacy, a top-ranked conference held in San Jose, CA. The paper was in collaboration with Chaz Lever and Manos Antonakakis from Georgia Institute of Technology and Davide Balzarotti from Eurecom, France. The work, that can be found here, performs a large-scale analysis of malware network communication using 26.8 million malware samples in combination with over 5 billion DNS queries collected from a large North American internet service provider (ISP). Among other, they discover that domains contacted from malware are observed in ISP network traffic often weeks or months before the malware shows up in the malware feeds. They also show that potentially unwanted programs (PUPs) rely on a surprisingly stable DNS and IP infrastructure.
The paper has been recently presented at the 40th M3AAWG General Meeting in Lisbon on June 15th.
IMDEA researcher Juan Caballero will be giving a talk at the 40th M3AAWG General Meeting in Lisbon on June 13th. The Messaging, Malware, Mobile, Anti-Abuse Working Group (M3AAWG) is the largest industry association working against botnets, malware, spam, viruses, DoS attacks and other abuse. It comprises over 200 companies including (among many others): Apple, AT&T, Comcast, Facebook, Google, LaCaixa, LinkedIn, Microsoft, Orange, and Yahoo.
This year the European Research Concil (ERC) celebrates its 10th anniversary. Fundación Madri+d para el conocimiento organizes is celebrating the event in Madrid on June 12, where two ERC grantees (Alexey Gotsman and Aleks Nanevski) from IMDEA Software Institute are taking an active role.
The IMDEA Software Institute is currently involved in the organization of two Summer Schools:
IMDEA Software Institute faculty Alessandra Gorla and PhD student Paolo Calciati received a Distinguished Paper Award at the 10th Seminar on Advanced Techniques & Tools for Software Evolution (SATToSE) that took place in Madrid on 79 June. The paper is entitled “How do Apps Evolve in Their Permission Requests? A preliminary Study” and was recently published at the 14th International Conference on Mining Software Repositories.
IMDEA Software Institute Phd student Luca Nizzardo, together with his colleagues Matteo Campanelli (City College of New York) and Steven Goldfeder (Princeton University), coordinated by Professor Rosario Gennaro (City College of New York), showed that Zero-Knowledge Contingent Payments (ZKCP), a well-known protocol for the fair exchange of digital goods over the blockchain, is insecure in its current form. In their last paper, after showing a practical attack, they propose a fix for ZKCP, and also extend this primitive to a new class of problems. The result has been recently highlighted both by the Zcash Blog and the Princeton "Freedom to Thinker" Blog. The research project has been developed at Center For Algorithms and Interactive Scientific Software (CAISS), directed by Rosario Gennaro at City College of New York, in Spring 2017. Luca's stay at CAISS has been funded both by City University of New York and the IMDEA Software Institute.
Gilles talk, entitled 'Advances in computer-aided lcryptography' presented recent developments in computer-aided cryptography which aims to provide rigorous tools that ease the design, analyze and implement cryptographic primitives and protocols.
Gilles' slides can be found here.
Manuel Carro participated in the Thought Leadership Workshop organized by NESSI, the European Platform on Software, Services, and Data organized in Brussels on May 31st and June 1st. Attendance to the meeting was by invitation, and the attendees discussed strategic topics for the ICT field in the forthcoming FP9 European program, in order to prepare a white paper to be presented to the Commission by NESSI.
The IMDEA Software Institute participated in the MC – COFUND Infoday, an informative event organized by the MINECO European Office aimed at giving information on how to manage a COFUND programme to the Spanish COFUND beneficiaries (FP7 and H2020). The event included the attendance by Alan Craig (EC - Marie Curie representative), who gave a presentation of the current 2017 call.
Juan José Collazo, Project Manager of AMAROUT II fellowship Programme, presented the Programme's results. AMAROUT II is coordinated by the IMDEA Software and includes the participation of the seven IMDEA Institutes. The programme is cofunded by an FP7 MC-COFUND.
After more than 10 years dedicated to the creation and development of the IMDEA Software Institute, Manuel Hermenegildo, founding director, stepped down to devote more time to research. He has been promoted by the Boards to the rank of Distinguished Professor.
The Board of Trustees, with the unanimous support of the Scientific Advisory Board, appointed Manuel Carro, former Deputy Director, as the new director of the Institute. Dr. Carro is Associate Research Professor at the Institute since 2011 and is also Associate Professor at the Technical University of Madrid, where he obtained his PhD in Computer Science.
On May 12, 2017, hundreds of thousands of computers worldwide were targeted by the infamous WannaCry attack. Would it have been possible to avoid it by means other than installing a patch to the affected Windows operating systems? Can similar situations be prevented rather than cured? Security researchers from the IMDEA Software Institute explore in this document what cutting-edge computer science can do now and what could be done in the future.
Several researchers from the IMDEA Software Institute are giving lectures in prestigious Summer schools around the globe:
IMDEA Software Institute researcher Manuel Hermenegildo give an invited talk on April 29 on Energy Consumption Analysis and Verification at the Fifth International Workshop on Verification and Program Transformation, VPT 2017, in Uppsala, Sweden, as part of the 20th European Joint Conferences on Theory and Practice of Software, ETAPS 2017.
The idea: “Private Common Data Analytics” by IMDEA student Bogdan Kulynych has been awarded a diploma in the competition actuaupm, a competition to create startups from the Polytechnical University of Madrid. The idea proposes to use advanced cryptographic techniques to enable companies to find commonalities in their data and analyze them jointly, without revealing anything about other data that is not common.
The IMDEA Software Institute has published its 2016 Annual Report.
IMDEA Software Institute director Manuel Hermenegildo has attended the Signing ceremony of the UNESCO/INRIA partnership - Preservation and sharing of Software Heritage. The signing ceremony took place in presence of UNESCO’s Director-General and the President of the French Republic, François Hollande. Manuel Hermenegildo attended the ceremony both as the IMDEA Software Institute representative and as a member of the INRIA scientific advisory board.
It is our great pleasure to welcome Professor Roberto Giacobazzi of the University of Verona, Italy as an IMDEA Software Institute visiting faculty member.
Prof. Giacobazzi has been appointed to the eminent role of Chair of Excellence by the Department of Education, Youth and Sports of the Community of Madrid.
Roberto is best known for his extensive and foundational work on abstract interpretation: both in the general theory, and in its applications to program semantics, static program analysis, language-based security, digital asset protection, and malware analysis, among other things. Roberto is the author of over 100 publications in international journals and conferences, and serves on the steering committees of the ACM Symposium on Principles of Programming Languages (POPL) and the Static Analysis Symposium (SAS).
The Ms. Thesis: “Code Search: A Semantic, Abstract-Interpretation Based Approach” by IMDEA student Isabel García has been awarded the first edition of the SISTEDES/Accenture Technology Best Master Thesis prize in Software Development Tools and Methodologies.
The thesis was developed at the IMDEA Software Institute under the supervision of Manuel Hermenegildo and José Francisco Morales within the Master's program on Artificial Intelligence at the Technical University of Madrid.
The prize will be received by Isabel during the SISTEDES 2017 Days (Jornadas SISTEDES 2017) in July 2017, in Tenerife, Spain.
Isabel's Ms. Thesis proposes a novel solution to finding code to reuse in large databases, based on the semantic properties of the code, and a novel query language for expressing such properties.
The semantic nature of the approach is based on the use of abstract interpretation, in contrast with current approaches that are basically syntactic.
An implementation is also provided to check the practical viability of the approach using the Ciao multi-paradigm programming language.
Thanks to the recent acquisition of Dark Fiber, REDIMadrid has been able to migrate the traffic of the High Energy group of the Universidad Autónoma de Madrid (UAM) to the dedicated network LHCONE (Large Hadron Collider Open Network Environment). The LHCONE network is a dedicated network for LHC machines of tier 1, 2, and 3 that enables the separation of LHC traffic from other traffic generated by machines that do not belong to the LHC. The migration was successfully performed on the 15th of March without any incidence. The new network provides the group with 10Gbps for sending and receiving LHC related traffic.
REDIMadrid, funded by the Madrid Regional Government and managed by the IMDEA Software Institute, currently provides high-speed connections at up to 10 Gbps to the universities and research institutes located in the Madrid region.
The goal of the project, entitled "DataMantium: Computación y comunicaciones seguras en la nube para entornos hostiles", is to develop security mechanisms to protect the integrity and privacy of users' data and processes in untrusted cloud scenarios. The results of the project are specially relevant in cybersecurity and digital trust, including aspects such as cryptography, to protect the information’s confidentiality and integrity, and the development of communication technologies in private and secure networks. The project includes the participation of IMDEA Software researchers Carmela Troncoso and Dario Fiore.
The IMDEA Software Institute participates in "Con ciencia en la escuela", a divulgative event aimed at bringing science nearer to the public at large. The Institute presents three demos in which attendees learn about Cryptography, Side Channel attacks on Web browswers and automated testing.
The event is organized by Círculo de Bellas Artes and FUHEM, with the collaboration of madri+d, Editorial SM, Cooperativa de Enseñanza José Ramón Otero, Consejería de Educación, Juventud y Deporte de laComunidad de Madrid, and Spanish Foundation for Science and Technology (FECYT) .
EIT Digital has today opened a node in Madrid to strengthen development of digital innovation in Spain. Tibor Navracsics, Commissioner for Education, Culture, Youth and Sport and Íñigo Méndez de Vigo, Spanish Minister for Education, Culture, and Sport, attended the opening at the IMDEA Software Institute and welcomed the closer integration of the Spanish innovation ecosystem into the European market through the new EIT Digital Node.
EIT Digital officially announced today that Madrid has become a full Node as of January 1, 2017. The Madrid Node now has the same rights as the eight other European Nodes of EIT Digital (Berlin, Eindhoven, Helsinki, London, Madrid, Paris, Stockholm and Trento), which offers great opportunities for Spain in driving forward digital transformation across Europe. EIT Digital has been present in Spain via its Madrid Associate Partner Group (APG) since 2013. Over four years from 2013-16, nearly €20 million was invested in Spain. Becoming a full Node enables a faster expansion of activities as is demonstrate by the fact that €15 million is being invested in 2017 alone in Spanish Innovation & Entrepreneurship as well as Entrepreuneurial Education activities.
Tibor Navracsics, Commissioner for Education, Culture, Youth and Sport, stated: "Innovation brings global benefits, but it begins with people at local or regional level. By establishing this Node in Madrid, EIT Digital is creating new opportunities in the region, providing space where researchers, entrepreneurs and educators can learn from each other and produce innovative new products and services - and educating the next generation of young thought leaders." Willem Jonker, CEO of EIT Digital, said: "I am very happy with the establishment of a full Node in Spain, which enables a significant increase of our innovation and entrepreneurial education activities in Spain."
EIT Digital's Spanish partners include Atos, the IMDEA Software Institute, Indra, Ferrovial, the Technical University of Madrid (UPM), Nokia-Spain and Telefonica.
IMDEA Software researcher Juan Caballero will be part of an effort to develop an online banking anti-fraud system. This work is supported by the EIT Digital’s 'Digital Finance' Action Line.
The “Online banking anti-fraud monitoring” innovation activity is one of three innovation activities of the Digital Finance Action Line of EIT Digital in 2017. Digital Finance, also known as “FinTech” focusses on the delivery of innovative financial products and services through digital technology, with the objective of making financial systems more reliable, more transparent and customer friendly improving thus the banking experience for the people in the society and the reducing the dependency of banks on central infrastructures.
Coowry a startup enabling easy micro payments whose offices are located in the IMDEA Software building was featured in the Spanish newspaper ABC.
IMDEA Software Institute researcher Carmela Troncoso has participated in the 2nd INTERPOL Workshop on Privacy Enhancing Technologies held on the 30th of January in Lyon, France. Carmela's talk, entitled “Privacy-preserving systems: Systematic reasoning for design and evaluation.” explained how to tackle the system engineering problem from a privacy point of view, describing means to reason about embedding strong privacy guarantees into ICT systems, and means to approach the evaluation of private information leakage in such scenarios.
IMDEA Software Institute researcher Dario Fiore has won with colleagues Michael Backes (DE), Manuel Barbosa (PT), and Raphael M. Reischuk (CH) the first edition of the CNIL/Inria prize on privacy protection for their publication entitled “ADSNARK: Nearly Practical and Privacy-Preserving Proofs on Authenticated Data.” This prize was jointly organized by the CNIL and Inria, two french government bodies.
IMDEA Software Institute researcher Boris Köpf will be lecturing at the Spring school on “Security & Correctness in the Internet of Things 2017” that is going to be held from May 8th to May 12th in Graz, Austria.
The five winners of the EIT Digital Summer School Competition on Privacy, Security and Trust for the best project have visited EIT Digital Madrid Node located at IMDEA Software Institute as part of their prize. During their visit they have met researchers from IMDEA Software, Carmela Troncoso and Dario Fiore, who explained to them the Institute's activities in the field of privacy and cybersecurity and gave feedback about the security aspects of the potential new product that the winners have developed during their summer school. In addition to the research-oriented meeting, they also met the local Business Accelerator team and visited the cybersecurity business unit of Telefonica.
IMDEA Software Institute faculty member Aleks Nanevski receives a prestigious ERC Consolidator Grant for the project "Mathador - Type and Proof Structures for Concurrent Software Verification".
Concurrent programs are notoriously difficult to write because of the complexity of interaction between their components. This complexity comes into the sharpest focus if one tries to develop a mathematical, computer-checkable, proof that a concurrent program produces the desired result. The required effort for developing such a proof today is overwhelming even for the simplest concurrent programs, because of the combinatorial explosion associated with the component interaction.
The goal of the Mathador project is to study, decompose, and simplify the structure of mathematical proofs of concurrent programs, to the point where they can be developed on a regular basis. Mastering these proofs will mean that we know how to describe the interaction between concurrent components in an intellectually manageable way. In turn, this will directly impact how we think about, write, and understand concurrent software.
Sonia Belaid received the prize “Trophées des ingénieurs du futur” organized jointly by the publications “Industrie & Technologies” and “Usine Nouvelle” for the work in her thesis “Security of Cryptosystems Against Power-Analysis Attacks”. This thesis includes the work on verifying the security of masked algorithms against differential power analysis, done in collaboration with Gilles Barthe and former IMDEA Software Institute researchers François Dupressoir and Pierre-Yves Strub.
EIT digital organized a match-making event on Cybersecurity that took place at the IMDEA Software Institute. Five large companies (ATOS, Ferrovial, Indra, Scytl and Telefonica/11Paths) set out Cybersecurity-related challenges to which ten start-ups and two research organizations (IMDEA Software Institute and Universidad Politécnica de Madrid) have responded presenting their technology, products, and ideas in order to meet these challenges. The match-making event begun with a keynote by IMDEA Software Institute faculty members Juan Caballero and Carmela Troncoso.
IMDEA Software Institute faculty Boris Köpf and Juan Caballero, after a successful review process involving high-level international external examiners, have been promoted to the rank of Associate Research Professor. The promotion was approved by both the Scientific Advisory Board and the Board of Trustees.
A paper by IMDEA Software Institute PhD student Nataliia Stulova, and researchers José Francisco Morales and Manuel Hermenegildo, entitled “Reducing the Overhead of Runtime Checks via Static Analysis”, received the highest score among all accepted papers at the 18th International Symposium on Principles and Practice of Declarative Programming, PPDP 2016 held in Edinburgh, Scotland UK, co-located with the 26th International Symposium on Logic-Based Program Synthesis and Transformation, LOPSTR and the 23rd. Static Analysis Symposium, SAS.
Researchers at the IMDEA Software Institute presented two papers at the 32nd International Conference on Logic Programming (ICLP'16), held in New York, which are published in a special issue of the "Theory and Practice of Logic Programming" (TPLP) journal, and one more at the ICLP affiliated Doctoral Consortium on Logic Programming. ICLP is the top international venue for the area of logic programming.
First, PhD student Isabel García together with researchers José Francisco Morales and Manuel Hermenegildo have a paper, entitled "Abstract Code Search", that presents a novel code search technique based on querying for automatically inferred semantic properties of the code, rather than its syntactic or structural properties.
Second, researcher Pedro López-García together with PhD students Maximiliano Klemen and Umer Liqat, and researcher Manuel Hermenegildo have a paper entitled "A General Framework for Static Profiling of Parametric Resource Usage" describing an implementation of a novel framework for setting up cost equations/relations for performing a wide range of resource usage analyses aimed at performing static code profiling. This new approach is much more relevant to code optimization that previous resource inference approaches.
Third, PhD student Joaquín Arias presents his research at the 12th ICLP Doctoral Consortium (DC-ICLP), a forum for doctoral students working in areas related to logic and constraint programming, held as part of the main ICLP'16 conference. His work, entitled "Tabled CLP for Reasoning over Stream Data", will be published by Dagstuhl Publishing in the OpenAccess Series in Informatics (OASIcs).
The IMDEA Software Institute invites applications for 2 positions to work in the recently funded ElasTest Horizon 2020 project. One position is in the area of Security and the other in the area of Runtime Verification, both on the context of testing large cloud applications.
Both positions are at the Post-doctoral or Ph.D. student level. Candidates can select at which level they want to apply. Both positions start on January 2017 (later start dates can be negotiated) and last 2 to 3 years for post-docs and up to completion of studies for Ph.D. students.
Further information can be found here.
Manuel Carro, deputy director of the IMDEA Software Institute, is the PC Co-Chair of 2016 International Conference on Logic Programming (ICLP'16), the premier international conference for presenting research in logic programming and related areas. ICLP'16 will take place in New York City from October 18 to October 21, with pre-conference workshops and the Autumn Schools on Computational Logic on the 16th and 17th. The detailed program is available here.
The European Researchers' Night in Madrid 2016, coordinated by the madrimasd Foundation for Knowledge, is an action financed by the European Comission, celebrated in over 300 european cities at a time. Twenty scientific institutions in Madrid, including the IMDEA Institutes, collaborated this year.
More details in the extended news at IMDEA.org
IMDEA Software Institute researchers Juan Caballero and Dario Fiore were invited speaker at the GSE Management summit that took place in Lisboa, Portugal, 26-27 September. Dr Juan Caballero's talk was entitled “CyberProbe and AutoProbe: Towards Internet-Scale Active Detection of Malicious Servers”. Dr Dario Fiore's was giving a talk with the title “Modern Cryptography for Privacy and Integrity in the Cloud”.
Carmela's talk, that can be found here, describes systematic ways to reason about privacy when engineering systems. The first part of the talk makes explicit which are the design strategies followed by privacy experts when engineering privacy-preserving systems, and shows how these design strategies require the use of Privacy Enhancing Technologies. The second part describes systematic approaches to develop such technologies in an optimal manner to support the implementation of privacy by design.
The IMDEA Software Institute faculty member Dario Fiore, coauthors two papers to appear at important Cryptographic conferences.
The first, together with Anca Nitulescu from ENS Paris, is accepted at the 14th Theory of Cryptography Conference (TCC 2016-B). This work, entitled “On the (In)security of SNARKs in the Presence of Oracles”, studies and sheds light on the security properties of efficient cryptographic proof systems. The work was partially done while A. Nitulescu was a research intern at IMDEA Software Institute.
The second, co-authored by IMDEA Software's PhD student Luca Nizzardo, together with Katerina Mitrokotsa and Elena Pagnin from Chalmers University, is accepted at the 22nd Annual International Conference on the Theory and Applications of Cryptology and Information Security (ASIACRYPT 2016). This work, entitled “Multi-Key Homomorphic Authenticators”, proposes new cryptographic mechanisms that allow for certifying the correctness of data and computations.
The IMDEA Software Institute will participate in a newly funded Horizon 2020 EU project called ElasTest: an elastic platform for testing complex distributed large software systems. The ElasTest project will develop infrastructure to help developers test and validate “software in the large”, while maintaining compatibility with current practices and tools. ElasTest will use a combination of instrumentation, test orchestration and test recommendation specifically crafted for improving the software reliability in the large software and in particular for cloud applications. The ElasTest consortium involves 11 companies, universities, and research centers from 6 European countries. The IMDEA Software Institute involvement focuses on runtime verification (Dr. César Sánchez) and security (Dr. Juan Caballero). The project will launch on January 2017 and will last for 3 years.
Four papers by IMDEA Software Institute researchers have been accepted for publication at the 23rd ACM Conference on Computer and Communications Security to be held in Vienna, Austria, at the end of October:
Dario Fiore's work, entitled "Hash First, Argue Later: Adaptive Verifiable Computations on Outsourced Data", is co-authored by Cédric Fournet, Markulf Kohlweiss, Olga Ohrimenko and Bryan Parno from Microsoft Research, and Esha Ghosh from Brown University. This paper proposes new cryptographic schemes that enforce third parties to perform computations correctly.
The other three papers are co-authored by IMDEA Software Institute faculty member Gilles Barthe and former faculty member Pierre-Yves Strub. The first paper, "Advanced Probabilistic Couplings for Differential Privacy", with Noémie Fong (ENS & IMDEA Software Institute), Marco Gaboardi (University at Buffalo, SUNY), Benjamin Grégoire (Inria), and Justin Hsu (University of Pennsylvania), provides new techniques to formally verify differentially private algorithms.
On the same vein, their second paper: "Differentially Private Bayesian Programming", with Gian Pietro Farina and Marco Gaboardi (University at Buffalo, SUNY), Emilio Jesús Gallego Arias (CRI Mines – ParisTech), Andrew D. Gordon (Microsoft Research), and Justin Hsu (University of Pennsylvania), presents novel means for writing and verifying differentially private Bayesian machine learning algorithms.
Finally, their third paper, "Strong non-interference and type-directed higher-order masking", with Sonia Belaïd (Thales Communications & Security), Pierre-Alain Fouque (Université Rennes 1), Benjamin Grégoire (Inria), Rebecca Zucchini (Inria), and François Dupressoir (former IMDEA Software Institute member), presents a fully automated methodology to verify the probing security of masked algorithms against differential power analysis, and generate masked versions from unprotected descriptions of an algorithm.
More information at CCS 2016.
IMDEA Software Institute’s researchers Manuel Hermenegildo and Pedro López-García, were the Program Committee chairs of the 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016) held in Edinburgh, Scotland UK, September 6-8, 2016, co-located with 18th International Symposium on Principles and Practice of Declarative Programming, PPDP, and the 23rd. Static Analysis Symposium, SAS. The program can be found here. The International Symposium on Logic-Based Program Synthesis and Transformation aims to stimulate and promote international research and collaboration in logic-based program development in any language paradigm.
IMDEA Software Institute faculty member Alexey Gotsman receives a prestigious ERC Starting Grant. His project is called RACCOON - A Rigorous Approach to Consistency in Cloud Databases.
IMDEA Software Institute faculty Juan Caballero has been selected as member of the editorial board of the ACM Transactions on Privacy and Security (TOPS) journal. ACM TOPS publishes high quality research results in the fields of information and system security and privacy. Previously known as ACM TISSEC, it was recently renamed to include the areas of privacy and data protection.
The IMDEA Software Institute invites applications for one PhD position in the area of Cryptography and four Postdoc positions in the areas of Cryptography, Anonymity, Privacy, Programming Languages, Verification, and Side-channel Attacks.
The successful PhD candidate will do research in cryptography under the supervision of Dario Fiore. Postdoc candidates can work with one of the following faculty members Gilles Barthe, Dario Fiore, Boris Köpf, Carmela Troncoso.
Further information can be found here.
AVClass automates a common task performed by malware analysts. It takes as input the AV labels for a large number of malware samples (e.g., VirusTotal JSON reports) and it outputs the most likely family name for each sample that it can extract from the AV labels. It can also output a ranking of all alternative names it found for each sample.
The design and evaluation of AVClass is detailed in an upcoming RAID 2016 paper: AVClass: A tool for Massive Malware Labeling. Marcos Sebastián, Richard Rivera, Platon Kotzias, and Juan Caballero. In International Symposium on Research in Attacks, Intrusions and Defenses, September 2016.
The IMDEA Institutes signed the agreement that seals their collaboration in the European Researchers' Night 2016.
The European Researchers' Night is an EU project that tries to bring researchers closer to society. The 2016 edition will take place simultaneously in more than 300 European cities on September 30th. In Madrid, and coordinated by the MadrI+D foundation, 20 academic and scientific institutions will develop 72 activities open to the entire public.
This year, the IMDEA Institutes participation will have as lead theme "A very Sporty Science or a very Scientific Sport", and will occur in the Student Residence of the CSIC.
This activity is laid out as the simulation of what happens in the Olimpics after a competition finishes. Researchers from all seven IMDEA Institutes will be interviewed as medalists in their sports. We will have a closer look at their sport interests and how they impact their work, the parallelism between science and sport, and more that will be uncovered in the Researchers' Night -- including live questions from the audience.
Hasser Veramendi has sucessfully defended his Master Thesis 'Privacy Implications of Open Data' co-supervised by IMDEA Software Institute Researchers Manuel Carro and Carmela Troncoso. The thesis was carried out in the framework of the European Master in Software Engineering from the Technical U. of Madrid (UPM).
Last Tuesday the EU Commission published an agreement on a new Public-Private Partnership on Cybersecurity with the European Cyber Security Organisation (ECSO), of which the IMDEA Software Institute is a founding member. This PPP is expected to trigger €1.8 billion of investment by 2020.
ECSO is an pan-european industry-led organisation with members including a wide variety of stakeholders such as large European companies, SMEs and Start-ups, users and operators, research centres, universities, clusters and associations as well as European Member State’s local, regional, and national administrations, countries part of the European Economic Area (EEA) and the European Free Trade Association (EFTA) and H2020 associated countries. ECSO collaborates with the European Commission and national public administrations to promote Research and Innovation (R&I) in cybersecurity and will have a key role in establishing the European Strategic Research and Innovation Agenda on Cybersecurity and a Multiannual Roadmap.
The IMDEA Software Institute has participated on the first ECSO General Assembly last week in Brussels, where the governing boards were elected. The representative of RENIC, the Spanish Network of Excelence for Cybersecurity Research, of which the IMDEA Software Institute is also a founding member, has been elected to be part of the Board of Directors.
The IMDEA Software Institute participates in the establishment of the Spanish Network of Excelence for Cybersecurity Research (Red Nacional de Excelencia en Investigación en Cyberseguridad, RENIC), becoming a founding member. RENIC has been founded by 16 Spanish entities, including Universities, and Research and Development Centers, that perform research in security-related topics.
The EIT Digital Madrid Co-Location center at the IMDEA Software Institute has hosted the EIT Digital Master Science and Online I&E education workshop which took place on June 4-5.
The workshop was organized by Gonzalo Leon (I&E Coordinator, EIT Digital Madrid and Director of UPM's CAIT), and Susana Eiroa (DTC Lead EIT Digital Madrid, IMDEA Software Institute).
The event gathered the representatives of EIT Digital I&E education programs all around Europe in order to coordinate on education design approaches including new I&E strategies. Attendees included the Madrid I&E education team (Gonzalo León, Alberto Tejero and Arístides Senra, UPM’s CAIT), as well as Frederic Renouard (EIT Digital I&E Coordinator and head at the Rennes satellite), Olli-Pekka Mutanen (Aalto University), Erik Jensen (TU Delft), Jean-Michel Dalle (UPMC), Matteo Bonifacio (U. Trento), Farideh Heidari (TUE), Adam Tarsci (ELTE) and Terrence Brown (KTH).
IMDEA Software Institute faculty Pierre Ganty is giving an invited lecture at the “Cursos de Verano, Matemáticas para el mundo y para la sociedad”. The school is held June 27-July 1, 2016 in San Lorenzo de El Escorial and Pierre is giving his lecture in the session dedicated to safe and secure systems.
IMDEA Software Institute faculty Boris Köpf, has chaired the Program Committee of the 29th IEEE Computer Security Foundations Symposium (CSF 2016) together with Michael Hicks from the University of Maryland. The selected program can be found here. The conference is held June 27-July 1, 2016 in Lisbon. The Computer Security Foundations Symposium is an annual conference for researchers in computer security. CSF seeks contributions on foundational aspects of computer security as well as their application to practice.
Several researchers from the IMDEA Software Institute are giving lectures in prestigious Summer schools around the globe:
IMDEA Software Institute faculty member Alessandra Gorla, along with Vitalii Avdiienko, Konstantin Kuznetsov, and Andreas Zeller (Saarland University), and Steven Arzt, Siegfried Rasthofer, and Eric Bodden (TU Darmstadt), has received a Special Mention at the Spanish national conference “Jornadas Nacionales de Investigacion en Ciberseguridad” (JNIC 2016). The awarded work is entitled: "Abnormal sensitive data usage in Android apps".
Another two papers from the IMDEA Software Institute have been presented at the conference: Ayudante: Identifying undesired variable interactions (Abstract). Irfan Ul Haq, Juan Caballero and Michael D. Ernst (University of Washington); and "Engineering privacy by design reloaded", by Carmela Troncoso with Seda Gurses (Princeton University) and Claudia Díaz (K. U. Leuven).
On June 7th over 20 researchers from different Spanish institutions (IMDEA, URJC, UPM, UAH, EHU, UCLM and Bitergia) met at the IMDEA Software Institute for the first Madrid Seminar on Empirical Software Engineering (MadSESE). Sandro Morasca (Università dell’Insubria, Italy) gave a keynote during the event. More information about the event here.
PhD students Juan Manuel Crespo and Goran Doychev graduated. Both students obtained their degree from the Technical U. of Madrid (UPM) within the DSS doctoral program, in which IMDEA faculty collaborate.
Juan Manuel defended his thesis entitled "Automation and Modularity of Cryptographic Proofs in the Computational Model". During his studies, he was advised by IMDEA Software Institute faculty member Gilles Barthe. His work proposes new methods to develop automated cryptographic proofs in a cost-effective manner, without sacrificing rigour and obtaining end to end guarantees.
Goran's thesis "Tools for the Evaluation and Choice of Countermeasures against Side-Channel Attacks" was supervised by IMDEA Software Institute faculty member Boris Köpf. His thesis focuses on the development of tools to support designers and implementers at the time of choosing the best countermeasures to avoid information leakage through side channels during the execution of cryptographic protocols.
The IMDEA Software Institute has published its 2015 Annual Report.
IMDEA Software Institute researchers Alexey Gotsman and Andrea Cerone received the best paper award at the ACM Symposium on Principles of Distributed Computing (PODC 2016) for their work entitled “Analysing Snapshot Isolation”.
The third Workshop of the Joint Research Center between Microsoft Research and the IMDEA Software Institute takes place May 3-4, 2016, at Microsoft Research Cambridge, UK. The workshop is aimed at discussing collaborative work on chosen software projects and, where possible, to bring those advances to Microsoft's businesses.
The workshop focuses on the following three projects:
It is organized by Judith Bishop and Markulf Kohlweiss from Microsoft Research and by Manuel Hermenegildo and Alexey Gotsman from the IMDEA Software Institute.
The 2-day workshop includes the following keynote speakers:
Dr. Brian A. LaMacchia “bal” to his friends is the Director of the Security \& Cryptography group within Microsoft Research (MSR), where his team conducts basic and applied research and advanced development. Brian is also a founding member of the Microsoft Cryptography Review Board and consults on security and cryptography architectures, protocols, and implementations across the company. Before moving into MSR in 2009, Brian was the Architect for cryptography in Windows Security, Development Lead for .NET Framework Security, and Program Manager for core cryptography in Windows 2000. Prior to joining Microsoft, Brian was a member of the Public Policy Research Group at AT&T Labs—Research.
Dr. Pierre Ganty is an Associate Professor (tenured) at the IMDEA Software Institute. He works on the verification of systems with infinitely many states, from theoretical foundations of automated analysis all the way down to algorithms and implementation. Pierre holds a joint PhD degree in Computer Science from the University of Brussels, Belgium and from the University of Genova, Italy, obtained in 2007. After his PhD, Pierre did a two year postdoc at the University of California, Los Angeles. Pierre joined the IMDEA Software Institute institute in the Fall of 2009 as a tenure-track assistant research professor.
Notiweb, the science and technology news publishing service of madri+d, published the piece “El Software: Cuando las nubes y las manzanas no son lo que parecen” about the research conducted by some of the researchers at IMDEA Software.
IMDEA Software Institute researchers Gilles Barthe and François Dupressoir, along with José Bacelar Almeida (Universidade do Minho and HASLab INESC Tec) and Manuel Barbosa (Universidade do Porto and HASLab INESC Tec), received the best paper award at the 23rd International Conference on Fast Software Encryption (FSE 2016) for their work entitled “Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC”.
IMDEA Software Institute’s Deputy Scientific Director, Manuel Carro, is coorganizer and chair of the Program Committee of the 1st Workshop on Program Transformation for Programmability in Heterogeneous Architectures (PROHA 2016). The workshop will be held March 12, 2016 in Barcelona, as a satellite workshop of CGO, and co-located with prestigious conferences such as HPCA, PPoPP, EuroLLVM, and CC. The workshop focuses on techniques and tools for program synthesis and transformation aiming at supporting the development and maintenance of programs for heterogeneous architectures.
Antonio Nappa defended his PhD thesis “Defending Against Cybercrime: Advances in the detection of Malicious Servers and the Analysis of Client-Side Vulnerabilities.” The thesis focuses on the analysis of two complementary aspects of cybercrime (i.e., computer crime perpetrated through the network to make money). These two aspects are the infected machines used to monetize the crime through different actions (i.e., clickfraud, DDoS, spam) and the server infrastructure used to manage these machines (e.g., C&C, exploit servers, monetization servers, redirectors). In the first part, the thesis investigates the victim machines analyzing which is their exposure to threats over time while, in the second part, Antonio proposes novel active probing techniques to detect and analyze malicious server infrastructures.
As part of the ongoing activities developed by the Madrid EIT Doctoral School, the Opportunity Recognition (OR) Seminar took place this week from the 22nd to the 26th of February, at the EIT Digital Madrid Co-Location center in the IMDEA Software Institute. The seminar was organized by Prof. Gonzalo Leon (Education Support, EIT Digital Madrid and Director of UPM's CAIT) and Dr. Susana Eiroa (DTC Lead EIT Digital Madrid and IMDEA Software)
The seminar is aimed at 1st and 2nd year doctoral students, with the purpose of providing them with the appropriate background to develop a business idea based on the work and ideas developed as part of their own doctoral theses.
The course focused especially on the structure of the ICT market in Europe and Worldwide, protection and exploitation of thesis outcomes, funding options, and business modeling.
The participants had the opportunity to meet experts in the innovation ecosystem, researchers and entrepreneurs. There were ample opportunities to exchange experiences and do networking, and also to have the students present their business ideas and work in groups.
During the week a series of lectures and talks were given by some key business executives, entrepreneurs, academic researchers and start-up mentors, such as Elisa Martín (Chief of Technology and Innovation, IBM), Amit Pau (MD Ariadne Capital & Entrepreneur Country Global; Partner, Ariadne Fund), Dr. Jesús Contreras (EIT Digital BDA – CLC Manager), David Pascual (Manager of Institutional Development of Innovation, INDRA), Carlos Otermin (Manager Business Incubator, CAIT UPM), Simón Viñals (Director of Technology at INTEL), Juan Polo (EMEA Enterprise Client Marketing Manager at INTEL), Prof. José Carlos González (CEO MeaningCloud LLC, Partner and Member Advisory Board Singular Meaning), among many others.
More info is available at:
The European Institute of Innovation and Technology (EIT) is opening a competitive call for new Knowledge Innovation Communities (KICs) in 2016. The Spanish agency Center for Industrial and Technological Development (CDTI) has invited Manuel Hermenegildo, director of the IMDEA Software Institute and of the EIT Digital Madrid APG, to share the successful experiences and best practices of the Spanish members within the EIT Digital KIC at a meeting at CDTI with potential Spanish applicant cosortia. The meeting was opened by the director of CDTI, Francisco Marín, and included also the participation of Michal Gorzynski, Head of the Monitoring Section at the EIT, and Josep Samitier, Director of the Institute for Bioengineering of Catalonia and of EIT Health Barcelona.
It was our great pleasure to welcome José Manuel Torralba Castelló, Director-General for Universities and Research, and Rafael García Muñoz, Deputy Director-General for Research, Regional Ministry of Education, Youth, and Sport of the Madrid regional government. They have visited our facilities and discussed with researchers progress in the different research lines.
NEXTLEAP is a recently approved H2020 European project which focuses on the development of an end-to-end secure messaging system with strong emphasis on privacy and freedom. The main technical outputs of the project to which the Institute will contribute are a Secure Address Book that does not leak user social contacts to any service provider, a Secure Communication Architecture that does not leak information to passive observers such as Internet Service Providers or Government Agencies, and a Private Data Analytics Module that allows for computation of statistics without revealing sensistive user information to any party.
Besides the IMDEA Software Institute, the NEXTLEAP consortium includes INRIA (France), University College London (UK), CRNS (France), IRI (France), and Merlinux, a Software Development SME from Germany.
Last Wednesday, February 10 the IMDEA Software Institute was delighted to host the visit of Dr. Charles J. Holland, the European representative of the U.S. Office of Naval Research Global (ONR Global).
The visit included a guided tour through the Institute facilities where Dr. Charles J. Holland had the opportunity to meet personally with several researchers, including the team working on the Syncrypt Project.
Syncrypt is a cybersecurity project coordinated at the IMDEA Software Institute by Gilles Barthe and Benedikt Schmidt, joint with Stanford University and The University of Pennsylvania, which has been awarded over one million dollars of funding from the U.S. Office of Naval Research.
IMDEA Software Institute’s Scientific Director, Manuel Hermenegildo, has chaired the Program Committee of the 25th International Conference on Compiler Construction (CC 2016). The selected program can be found here. The conference will be held March 17-18, 2016 in Barcelona, co-located with CGO, HPCA, PPoPP, and EuroLLVM. The International Conference on Compiler Construction publishes work on processing programs in the most general sense: analyzing, transforming and executing input that describes how a system operates, including traditional compiler construction.
IMDEA Software Institute PhD student Pepe Vila won the “shortest vector” prize in the annual Cross-Site Scripting Challenge (XSSMas Challenge) organized by the security company Cure53. The challenge consisted on exploiting new browser XSS vectors and bypassing several security checks and filtering mechanisms in the shortest possible way.
IMDEA Software Institute researcher Carmela Troncoso served as an invited panelist at the Computers, Privacy & Data Protection Conference (CPDP) in Brussels, Belgium. CPDP is the worldwide largest conference on Privacy and Data Protection, gathering more than 1000 attendees from diverse sectors such as regulators, policy makers, industry representatives and academic researchers.
Carmela participated in the panel organized by the European Commission, concretely DG Connect (European Commission Directorate General for Communications Networks, Content & Technology), named “Enhancing privacy and security through technological innovation” by giving a talk entitled “Seeing Privacy Enhancing Technologies as Business Enabling Technologies”. In this talk Carmela introduced advances on privacy technologies, such as those developed at the IMDEA Software Institute, that enable the design of ICT systems with the same functionality as those of today but without breaching users' privacy.
The IMDEA Software Institute is one of the main developers of CADENCE, an innovative service for recognition of threats evolved on complex networks which is now available on the market. CADENCE is a security service specifically designed for the detection of advanced persistent threats and targeted attacks.
CADENCE is an outcome of the EIT Digital Privacy, Security & Trust innovation activity led by Communication Valley Reply together with technology partners TNO and the IMDEA Software Institute.
Communication Valley Reply is the Reply Group company specialized in managed security services. TNO is an independent Dutch organization for applied research. TNO connects people and knowledge to create innovations that boost the sustainable competitive strength of industry and well-being of society.
The product was launched on December 9 in Milan.
Read the whole story from the EIT Digital website.
IMDEA Software Institute researchers Gilles Barthe and François Dupressoir have contributed to the discovery of vulnerabilities in Amazon’s open source security software, s2n, an open source implementation of the transport layer security (TLS) protocol. Together with IMDEA Software Institute researcher Michael Emmi they are working on automation for proving the absence of vulnerabilities in security protocol implementations, including s2n.
Read the whole story from the Amazon Web Services Security Blog.
Read more here.
IMDEA Software Institute hosted and co-organized the first EIT Digital seminar on "Raising Awareness in Innovation and Entrepreneurship." The seminar offers first year doctoral candidates of the EIT Digital Doctoral Training Centre (DTC) in Madrid a fresh view on how their doctoral theses can contribute to European innovation. The two-day course was organized by Susana Eiroa (Madrid DTC Lead, EIT Digital Madrid and IMDEA Software), Prof. Gonzalo León (Education Support, EIT Digital Madrid and UPM), and Jesús Contreras (BDA, EIT Digital and IMDEA Software), with the participation of Prof. Maurizio Gabbrielli (Head of the Doctoral School, EIT Digital).
The first day included presentations by Gonzalo León, Francisco Javier Elorza (Vice President for doctorate and post-graduate studies, UPM), and Maurizio Gabbrielli. In addition, PhD candidates presented their research ideas and plans towards their PhD. During the second day, representatives from academy and industry such as Prof. Juan José Moreno Navarro (Full Professor at UPM and regional MP), Daniel Concepción Sevillano (CTO of Banco Santander) and J.M. Leceta (Former EIT director) gave several talks on industrial PhDs and entrepreneurship. The day was closed with presentations from Radouane Oudrhiri (CEO Evolvys) and CEOs / CTOs from start-ups like Coowry, BioD, and DAIL Software.
More information at:
It was our great pleasure to welcome:
of the Madrid regional government, as well as all the other Board of Trustees members, who visited our facilities, discussed with IMDEA Software Institute researchers, and attended our Board of Trustees meeting as new board members.
The Board of Trustees is the governing body of the IMDEA Software Institute Foundation. It is in charge of guaranteeing that the foundational objectives are fulfilled and that the assets of the Institute are managed correctly.
IMDEA Software Institute researcher Carmela Troncoso served as an invited speaker at the Smart City Expo World Congress held in Barcelona. The event included an exhibition where companies showcased solutions ranging from devices to analytics products for smart cities, and a conference with keynotes and panels covering important topics for smart city development.
Carmela’s talk at the Privacy in the Smart City panel, entitled “Privacy-preserving Smart Cities: Utopia or Reality”, provided a technical overview of current challenges and prospective solutions to privacy in smart city infrastructures. Privacy is an important research topic at the IMDEA Software Institute.
The first pan-IMDEA Conference on Science, Industry and Society was celebrated in the facilities of the IMDEA Materials institute. The conference was opened by Ms. Cristina Cifuentes, President of the Madrid Regional Government. The main goal of the conference was to show civil society the achievements o date of the seven IMDEA Institutes in terms of attracting talent, the high-quality of their scientific output, and the tight collaboration with industry. Prof. David Warren of the State University of New York at Stony Brook, and president of the IMDEA Software Institute Board of Trustees and Scientific Advisory Board, gave the keynote address. Researchers from the seven IMDEAs made presentations describing research lines and achievements of the different IMDEA institutes. IMDEA Software Institute faculty member Boris Köpf represented the Institute at the event gave an overview of our research areas followed by a more in-depth presentation of the security and privacy line.
It is our great pleasure to welcome Carmela Troncoso as an IMDEA Software Institute researcher. Carmela received her doctorate in 2011 from the Katholieke Universiteit Leuven in Belgium, and has since served as S&P Technical Lead at the Centro Tecnolóxico de Telecomunicaciones de Galicia (GRADIANT). Her doctoral thesis “Design and Analysis Methods for Privacy Technologies” received the Best Ph.D. Thesis Award from the European Research Consortium for Informatics and Mathematics WG Security and Trust Management. She has been a visitor at numerous prestigious security research groups including Microsoft Research Cambridge, the Hatswich group at the University of Illinois at Urbana-Champaign, and at LCA1 at the École Polytechnique Féderale de Laussane.
Carmela is a co-author of more than 35 publications in peer-reviewed international conferences and journals. She has been program chair of the Hot Topics in Privacy Enhancing Technologies Workshop (HotPETs) in 2010 and 2011, and General Chair of the Privacy Enhancing Technologies Symposium in 2012. She has also served on over 10 program committees of international conferences, and reviewed articles for numerous international journals.
Four articles by IMDEA Software Institute researchers are slated for publication at the 2016 ACM Symposium on Principles of Programming Languages (POPL), a flagship conference in this important area, held next January in St. Petersburg, Florida.
IMDEA Software Institute faculty member Alexey Gotsman has a paper facilitating the construction of distributed software systems by providing a framework for reasoning over the implementation choices that guarantee varying levels of consistency between distant machines.
Faulty member Pierre Yves Strub’s article develops a new programming language fostering both provably correct and efficient code for critical applications like cryptography, an ability afforded by its design around mechanical verification.
Faculty member Michael Emmi’s article develops automation for inferring the specifications of software modules which enables automated testing and verification of the crucial implementations underlying countless software systems.
Visiting faculty member Somesh Jha’s article leverages probabilistic modeling in order to report possible errors to programmers at compilation time, focusing on those more likely to be actual errors at runtime.
More information including the full list of accepted articles can be found here.
IMDEA Software Institute faculty Boris Köpf, Juan Caballero and Dario Fiore each win prestigious grants from the Spanish Ministry of Economy and Competitiveness: two Juan de la Cierva Fellowships and one Ramon y Cajal Fellowship.
IMDEA Software Institute faculty Dario Fiore and PhD student Luca Nizzardo, along with Dario Catalano (University of Catania), received the best paper award in the category of short papers (which includes already published work) at the first “Jornadas Nacionales de Investigacion en Ciberseguridad” (JNIC 2015). The awarded work is entitled “Programmable Hash Functions go Private: Constructions and Applications to (Homomorphic) Signatures with Shorter Public Keys”.
The thesis studies the formal verification of temporal properties of safety and liveness of parametrized concurrent systems, with a special focus on programs that manipulate complex concurrent data structures in the heap. This work presents a formal framework based on deductive methods which cleanly separates the analysis of the program control flow from the data manipulated by the program. The program control flow is analyzed using novel specialized deductive verification techniques specifically designed for coping with parametrized systems. Starting from a concurrent program and a temporal specification, the techniques generate a finite collection of verification conditions whose validity entails the satisfaction of the temporal specification by any client system, in spite of the number of threads. Additionally, the thesis explores the construction of decidable theories equipped with decision procedures that can automatically check the generated verification conditions for some complex concurrent data structures. Finally, the whole framework is evaluated over some safety and liveness properties for a collection of mutual exclusion protocols and concurrent pointer-based data structures.
The European Researchers' Night in Madrid 2015, coordinated by the madrimasd Foundation for Knowledge, is an action framed under the Horizon 2020 European programme, celebrated in over 300 european cities at a time. Twenty scientific institutions in Madrid, including the IMDEA Institutes, collaborated this year.
More details can be found here.
It is our great pleasure to welcome Professor Somesh Jha of the University of Wisconsin, Madison as an IMDEA Software Institute visiting faculty member. Somesh is best known his visionary work in information security, formal methods, programming languages, software engineering, and computational finance. Somesh is the author of over 100 publications in international journals and conferences, a recipient of the 2015 CAV Award, and an NSF CAREER Award recipient.
Four papers by IMDEA Software Institute researchers have been accepted for publication at the 22nd ACM Conference on Computer and Communications Security, a top-ranked conference in this important area, held in Denver, CO.
IMDEA Software Institute faculty member Dario Fiore has a paper on homomorphic encryption together with D. Catalano (University of Catania, Italy). Their work proposes new techniques that enable third parties to compute over encrypted data, namely to evaluate a function without learning its inputs.
Faculty member Juan Caballero has two papers. One paper with visiting Ph.D. student Srdjan Matic from Università degli Studi di Milano and IMDEA Ph.D. student Platon Kotzias proposes an approach for deanonymizing hidden services in the TOR anonymity network. The other one with Ph.D. students Platon Kotzias and Richard Rivera, and visiting Ph.D. student Srdjan Matic analyzes digitally signed malware and potentially unwanted programs such as adware.
Faculty members Gilles Barthe and Benedikt Schmidt have a paper on formal proofs for pairing-based cryptography together with B. Grégoire (INRIA). Their work describes a new method and a new tool to perform such proofs automatically.
More information at CCS 2015.
The IMDEA Software Institute has been awarded the Syncrypt cybersecurity project. The project, featuring IMDEA Software Institute researchers Gilles Barthe and Benedikt Schmidt, is joint with Stanford University and The University of Pennsylvania, and has been awarded over one million dollars of funding from the US Office of Naval Research (ONR).
Read more from Madrid’s regional Ministry of Education and Research.
IMDEA Software Institute researcher Aleks Nanevski gave an invited tutorial at the 2015 Conference on Mathematical Foundations of Program Semantics (MFPS) held this June in Nijmegen, Netherlands. His tutorial covered Concurrent program semantics and separation logic. More information here.
IMDEA Software Institute researcher Pavithra Prabhakar and her student Ratan Lal have published their work on analyzing parameterized linear systems in the International Conference on Embedded Software (EMSOFT). EMSOFT is a top-ranked conference in the field of embedded software and it will be held this year in Amsterdam, The Netherlands. The acceptance rate this year for the conference is 25%. The work focuses on the computation of bounded error approximations of the reachable set, and uses it for safety verification of an important class of dynamical systems, namely, parameterized linear systems. The authors have applied this techniques for analyzing aircraft collision avoidance protocols with several aircraft.
IMDEA Software Institute faculty member Pierre Yves Strub, and coauthors Benjamin Beurdouche (INRIA), Karthikeyan Bhargavan (INRIA), Antoine Delignat-Lavaud (INRIA), Cedric Fournet (Microsoft Research), Markulf Kohlweiss (Microsoft Research), Alfredo Pironti (INRIA), and Jean Karim Zinzindohoue (INRIA), received the distinguished paper award at the 2015 IEEE Symposium on Security and Privacy (S&P ’15) for their research paper entitled “A Messy State of the Union: Taming the Composite State Machines of TLS”.
IMDEA Software Institute PhD student Antonio Nappa, along with researchers from the International Computer Science Institute in Berkeley CA and other researchers from Google Inc. received the distinguished practical paper award at the S&P ’15 for their practical contribution entitled “Ad Injection at Scale: Assessing Deceptive Advertisement Modifications”.
The official announcement is available here.
The first scientific meeting of the EU COST Action "Runtime Verification beyond Monitoring (ARVI)" has taken place in Valletta, Malta on April 9th and 10th. IMDEA Software Institute faculty member César Sánchez is a member of the management committee and a workgroup leader, and a leader in the COST Action proposal’s elaboration.
Runtime verification (RV) is a computing analysis paradigm based on observing a system at runtime to check its expected behavior. RV has emerged in recent years as a practical application of formal verification, and a less ad-hoc approach to conventional testing by building monitors from formal specifications.
The main goals of the action are:
to create an infrastructure that supports comparing tools and reusing existing infrastructure in runtime verification,
to explore potential impactful applications of runtime verification to industrial settings like hardware, medical devices, cloud computing, and even human centric systems, and
to explore challenging application domains for monitoring and runtime verification, such as hybrid systems and distributed systems.
Given the importance of computer-based industries in Europe, novel applications of RV have a large impact in terms of the new class of designs enabled and their reliability and cost effectiveness.
This COST Action is funded for 4 years, until 2018.
The thesis presents a novel, tool-supported model-driven methodology for developing secure data-management applications. With the methodology defined, developers proceed by modeling three different views of the desired application: its data model, security model, and GUI model. These models formalize respectively the application's data domain, authorization policy, and its graphical interface together with its behavior. Afterwards a model-transformation function automatically lifts the policy specified by the security model to the GUI model. Finally, a code generator automatically generates a multi-tier application, along with all support for access control, from the security-aware GUI model. Miguel Ángel García de Dios was advised by IMDEA Software Institute faculty member Manuel Clavel and obtained his degree from Universidad Complutense de Madrid.
Four papers by IMDEA Software Institute researchers have been accepted for publication in the proceedings of the 27th International Conference on Computer Aided Verification, a top-ranked conference in this important field, held this year in San Francisco, CA. These four papers are among 68 selected for publication from over 250 submissions.
IMDEA Software Institute faculty member César Sánchez has a paper on model checking “hyperproperties”, together with Bernd Finkbeiner and Markus Rabe from Saarland University, Germany. Their paper characterizes the precise complexity of the model checking problem for hyperproperties, and shows how to leverage existing state-of-the-art model checking tools to handle hyperproperty specifications, with applications to security, symmetry, and coding theory.
IMDEA Software Institute faculty member Boris Köpf has a paper together with Klaus von Gleissenthall ((TU Munich) and Andrey Rybalchenko (Microsoft Research) on verifying quantitative program properties, such as bounds on resource usage or information leaks. The core technical novelty is an SMT-based algorithm for synthesizing interpolants with cardinality constraints that relies on the theory of counting integer points in symbolic polytopes.
IMDEA Software Institute faculty member Michael Emmi’s contribution reports on the development of a tool for uncovering concurrency bugs in Android apps, a joint work with Burcu Kulahcioglu Ozkan and Serdar Tasiran of Koç University in Turkey.
IMDEA Software Institute faculty member Pierre Ganty has a paper on the automated verification of shared-memory asynchronous systems together with A. Durand-Gasselin, J. Esparza from TU Munich and R. Majumdar from . Their work classifies verification problems for liveness properties in shared-memory asynchronous systems from a computational point of view. These systems are characterized by a leader process and arbitrarily-many anonymous and identical contributors. Processes communicate through a shared, bounded-value register.
Find more information on the conference website.
IMDEA Software Institute faculty member John Gallagher and coauthor Bishoksan Kafle received the best paper award at the 2015 Workshop on Partial Evaluation and Program Manipulation (PEPM ’15) for their paper entitled “Constraint Specialisation in Horn Clause Verification”.
The article appears in the ACM Proceedings of the 2015 Workshop on Partial Evaluation and Program Manipulation (PEPM ’15), edited by Kenichi Asai and Kostis Sagonas: DOI.
The second Workshop of the Joint Research Center between Microsoft Research and the IMDEA Software Institute took place April 9-10, 2015, at the IMDEA Software building in Madrid. The workshop was aimed at discussing collaborative work on chosen software projects and, where possible, to bring those advances to Microsoft's businesses.
The workshop focused on the following three projects:
It was organized by Judith Bishop and Cedric Fournet from Microsoft Research and by Manuel Hermenegildo and Alexey Gotsman from the IMDEA Software Institute.
These workshops bring together researchers and students to discuss their collaborative work on hot topics in software in order to advance the state of the art and, where possible, to bring those advances to market.
The 2-day workshop included the following keynote speakers:
Phil Bernstein is a distinguished scientist in the Database Group of Microsoft Research Redmond. Bernstein is also an affiliate professor at the University of Washington and frequent committee member or chair of conferences such as VLDB and SIGMOD. He won the SIGMOD Edgar F. Codd Innovations Award in 1994. Bernstein is a member of the National Academy of Engineering and an elected Fellow of the Association for Computing Machinery. Currently, he is working on a distributed systems programming framework, called Project Orleans: Distributed Virtual Actors for Programmability and Scalability.
Aleks Nanevski is an Assistant Research Professor at the IMDEA Software Institute which he joined in the Fall 2009. Prior to that, Nanevski was a postdoctoral researcher at Carnegie Mellon University under the supervision of Prof. Edmund Clarke, at Harvard University under the supervision of Prof. Greg Morrisett, and at Microsoft Research, Cambridge. Aleksandar holds a PhD degree in Computer Science from Carnegie Mellon University, which he obtained in August 2004. He is working on type systems and structured proofs for concurrent software verification.
The IMDEA Software Institute has published its 2014 Annual Report.
The IMDEA Software Institute has been awarded an Honorable Mention in the area of Public-Private Cooperation by the madri+d Foundation, for its cooperation with the Italian industrial group Reply and Dutch TNO on cyber attack detector engineering and its commercial exploitation.
This collaboration was supported in part by Cadence, an EIT ICT Labs innovation activity in the area of privacy, security, and trust, started in 2014, in which the IMDEA Software Institute, TNO, and Reply are applying novel anomaly detection technologies to the creation of specific innovative products and services for providing more secure ICT environments for both governments and businesses.
This Honorable Mention was awarded by the madri+d Prizes jury in the tenth annual edition of these awards, which recognize significant scientific and technological advances in solving industrial and societal challenges, the capacity for converting research projects and results into wealth and welfare in the Madrid Region, excellence in implementing collaborative research and development activities on the European level, and the generation and dissemination of knowledge.
IMDEA Software Institute faculty researcher Pierre Yves Strub, together with his colleagues at INRIA Rocquencourt, France and Microsoft Research have uncovered a vulnerability in the popular SSL encryption mechanism used widely on the Internet to access web pages securely. The flaw, dubbed “FREAK: Factoring RSA Export Keys” can be exploited to trick web browsers into interacting with malicious websites. The problem affects a large number of web servers and clients and has thus received major media impact.
This discovery was made within the ongoing SMACK TLS project, which is aimed at developing increasingly-secure Internet authentication software. Pierre Yves Strub and his colleagues have developed an automated technique to discover vulnerabilities in implementations of authentication protocols, and uncovered several vulnerabilities which, gone unnoticed, could be exploited by hackers to compromise Internet security.
The researchers focused on the family of authentication protocols know as “Transport Layer Security” (TLS), which is the increasingly-popular successor to the ubiquitous “Secure Sockets Layer” (SSL) protocol family. By building formally-verified reference implementations of TLS protocols, they were able to systematically generate inadmissible protocol responses, which should be disallowed by the protocol, and test whether any of those responses were in fact admitted by existing implementations. Inadmissible responses suggest potential vulnerabilities, and were to converted into exploits in actual TLS implementations. “FREAK” is one of the vulnerabilities discovered.
More details can be found here.
This work was performed in collaboration with Benjamin Beurdouche, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Alfredo Pironti, and Jean Karim Zinzindohoue of INRIA Rocquencourt, France, and Cedric Fournet and Markulf Kohleiss of Microsoft Research.
Last Wednesday, February 18th, Lorena Heras Sedano, responsible for the General Directorate for Universities and Research of the Madrid Regional Government visited the premises of the IMDEA Software Institute with Juan Ángel Botas Echevarría, Deputy Director for Research.
The visitors were given a guided tour of the premises and they met personally the Institute's research team. Several researchers presented the goals and some of the advances attained in the different research lines of the Institute and the ongoing research projects, as well as their practical applications and other industrial collaboration and technology transfer activities.
They also visited the Microsoft - IMDEA Software Joint Research Center and the Madrid Co-location Center of the ICT Labs KIC of the European Institute of Innovation and Technology. This co-location center is also the headquarters of this KIC in Spain, and it is coordinated by the IMDEA Software Institute and located in its premises.
More info can be found here.
It is our great pleasure to welcome Professor Ben Livshits as an IMDEA Software Institute visiting faculty member. Ben is a research scientist at Microsoft Research and an affiliate professor at the University of Washington, USA, and is known for his work in software reliability, especially tools to improve software security, with a primary focus on approaches to finding buffer overruns in C programs and a variety of security vulnerabilities (cross-site scripting, SQL injections, etc.) in Web-based applications. He is the author of several dozen academic papers and patents. Lately, he has been focusing on topics ranging from security and privacy to crowdsourcing an augmented reality.
Four papers by IMDEA Software Institute researchers have been accepted for publication at the 36th IEEE Symposium on Security and Privacy, a top-ranked conference in this important area, held in San Jose, CA. These four papers are among 55 papers selected for publication out of over 400 submissions to the conference.
IMDEA Software Institute faculty member Dario Fiore has a paper on privacy-preserving proofs, together with M. Backes (CISPA, Saarland University), M. Barbosa (HASLab – INESC TEC and Universidade do Minho), and R. M. Reischuk (ETH Zurich). Their work (whose title is "ADSNARK: Nearly Practical and Privacy-Preserving Proofs on Authenticated Data") proposes a new system, called ADSNARK, that allows users to prove the correctness of computations while maintaining the privacy of the input data. The main novelty of ADSNARK is to work efficiently with authenticated inputs, a useful feature for applications such as smart metering and the emerging wearable computing paradigm.
Faculty member Juan Caballero and Ph.D. student Antonio Nappa have a paper on analyzing the lifecycle of software vulnerabilities in client applications (e.g., browsers, document editors). This work identifies several new threats presented by multiple installations of the same program and shared libraries. This work is collaboration with researchers at Symantec Research Labs and University of Maryland at College Park.
IMDEA Software Institute Ph.D student Antonio Nappa along with researchers from the International Computer Science Institute in Berkeley CA and other researchers from Google Inc. have a paper that presents a study on advertisement injection in browser session. They have developed a multi-staged pipeline that identifies ad injection in the wild and captures its distribution and revenue chains.
Faculty member Pierre Yves Strub has a paper on designing a generic, robust and verified state machine for the TLS protocol with Benjamin Beurdouche (INRIA), Karthikeyan Bhargavan (INRIA), Antoine Delignat-Lavaud (INRIA), Cedric Fournet (Microsoft Research), Markulf Kohlweiss (Microsoft Research), Alfredo Pironti (INRIA), and Jean Karim Zinzindohoue (INRIA). Their work addresses the problem of designing a robust composite state machine that can correctly multiplex between these different protocol modes of TLS. They present the first verified implementation of a composite TLS state machine in C that can be embedded into OpenSSL and accounts for all its supported ciphersuites. They also discovered several critical security vulnerabilities that have lain hidden, for years, in popular open-source SSL libraries.
More information at SP 2015.
The first edition of the Itinerant Cryptography Seminars, a multi-institutional series aimed at promoting cryptography research, was hosted by IMDEA Software Institute on January 22, and organized by Dario Fiore.
More details can be found here.
The International Competition on Software Verification (SV-COMP) is a driving force for the invention of new methods, technologies, and tools for the automated verification of computer software. Software verification is an unarguably-important research area as society becomes more and more dependent on its correct functionality: software bugs can cost lives and great monetary loss. Though the goal of verified software has existed since the dawn of computer science, the technology enabling widespread use of software verifiers has been extremely challenging to develop, due to fundamental philosophical limitations, practical engineering obstacles, and the challenge in surmounting both simultaneously. SV-COMP aims to advance software verification technology by bringing together the top international minds.
This year marks the 4th annual installment of an increasingly-competitive event, in which 22 entries from top research institutions including New York University, Ecole Normale Supérieure (ENS) of Paris, University of Freiburg, Tsinghua University, Microsoft Research, and IMDEA Software Institute compete across 13 categories of software verification problems.
Each competition entry is a computer program called a “verifier”, and each “problem” is a computer program whose correctness must be verified by the verifier. The verifiers are submitted as executable code, and the problems are provided as source code written in the C programming language. The verifiers classify problems either as “correct”, “incorrect”, or “unknown”, within a time limit of 900 seconds per problem. Points are awarded according to the accuracy of classification. In each problem category, the three highest-scoring verifiers are awarded medals: gold, silver, and bronze.
In collaboration with the University of Utah and Microsoft Research, the IMDEA Software Institute’s competition entry, named SMACK+Corral, was awarded medals in four categories — two gold, one silver, and one bronze — placing it among the top-performing verifiers. Only one entry earned more gold medals, and only three entries earned more medals total.
Technically, SMACK+Corral is the fusion of two programs. SMACK is an open-source project led by Zvonimir Rakamaric of the University of Utah, and Michael Emmi of the IMDEA Software Institute. The role of SMACK is to translate the C-language verification problems into mathematical representations which can be more-easily processed by automated logical-reasoning engines known as “theorem provers”. Corral, developed by Microsoft Research, applies novel reasoning algorithms to decide whether the given mathematical representation should be classified as “correct”. Combined, the two function as a powerful verifier of C-language programs.
The SV-COMP 2015 post-competition event is being held on the week of April 13th, 2015, as part of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), in London, UK. The event includes a short presentation by the authors of each entry, and an official announcement of the competition results.
More information at SV-COMP 2015.
On December 18, 2014, five students who won the contest at the EIT Digital Summer School in the field of Privacy, Security and Trust (PST) were invited to IMDEA Software Institute to present technological challenges and discuss their business ideas with the Institute's leading scientists. The students were:
The visit was organized and moderated by Jesús Contreras, EIT Digital Business Developer at the Madrid CLC.
On 18 December 2014, the Madrid CLC of EIT ICT Labs at IMDEA Software Institute hosted the FI-PPP-Liaison Demo Day, with presentations from the three SMEs that have won prizes from the FI-PPP Liaison project for using FI-WARE technologies to bring innovative products and services to the market:
SmartTaxi, with a smart app that helps taxi drivers reduce waiting time and to increase their customer pick up rate.
WeCollect (Wellness Telecom), who developed the eGarbage system to improve waste collection management.
B-SEED (Pyro Fire Extinction), with a platform to incorporate smart cities technologies into the natural environment, in order to improve prevention and management of forest fires.
The FI-PPP Liaison project connects EIT ICT Labs activities in the field of future networking solutions with FI-WARE as a major European initiative in developing and promoting new generation cutting-edge Future Internet (FI) technologies and solutions based on Public-Private Partnership (PPP).
The three companies have been awarded EUR 25,000 each to develop pilot projects based on Internet-of-Things (IoT) FI-WARE technologies, from pool of 40 applicants and 10 short-listed contenders which were provided with training and coaching within the FI-PPP Liaison project.
The demo day was organized by IMDEA Software Institute in cooperation with partners from Technical University of Madrid (UPM), Spain and Telefonica I+D, and was attended by other major actors in the IoT arena, such as Ferrovial.
On December 17, 2014, the IMDEA Software Institute organized an outreach event at the EIT Digital Madrid CLC to present the EIT ICT Labs Master School in ICT Innovation and its offer of post-graduate programs.
The Master School provides the highest level of international academic education in ICT with additional Innovation and Entrepreneurship (I&E) modules that enable the students to develop their own innovative ideas into new, marketable products and services. The overall goal is to boost EU entrepreneurship, and thus strengthen the basis of the innovation and technology-based economy.
Manuel Hermenegildo (Director of the IMDEA Software Institute and of the EIT ICT Labs Madrid Associate Node), and Juan José Moreno Navarro (UPM Vice-Rector for Graduate Studies and Deputy Director of the EIT ICT Labs Madrid Associate Node), hosted the event and explained the general guidelines of the Master programmes. UPM participates in the program as an affiliate university in Spain, together with another 19 top-level European technical universities.
The two-year Master programme is organized in eight technical majors, each executed by two distinct European universities. The programs are:
In addition to a full scholarship, summer school attendance, real professional experience in top IT companies, and mentoring for development of personal and team business projects and start-up creation, the graduates will receive a double degree from the implementing universities, and an official certificate in innovation and entrepreneurship from ICT Labs.
It is our great pleasure to welcome Alessandra Gorla as IMDEA Software Institute's newest Assistant Research Professor. Alessandra's doctoral dissertation from the Università della Svizzera Italiana, Lugano, Switzerland was awarded the Fritz Kutter Award for Best Industry-Related Thesis in Computer Science from a Swiss University in 2011. Her principal research interests are in malware detection for mobile applications, automatic software repair, and software testing and analysis.
The Joint EasyCrypt-F*-CryptoVerif School, which took place in Paris between 24 and 28 November 2014, attracted over 80 participants from Europe, North America and Japan. Easycrypt is the tool developed by researchers at IMDEA Software Institute led by faculty Gilles Barthe. The school was split between lectures, which introduced the formal foundations behind these tools, and exercises, where the participants used the tools to verify the security of representative cryptographic constructions.
See the full press release here.
It is our great pleasure to welcome Professor Roberto Giacobazzi of the University of Verona, Italy as an IMDEA Software Institute visiting faculty member. Roberto is best known for his extensive and foundational work on abstract interpretation: both in the general theory, and in its applications to program semantics, static program analysis, language-based security, digital asset protection, and malware analysis, among other things. Roberto is the author of over 100 publications in international journals and conferences, and serves on the steering committees of the ACM Symposium on Principles of Programming Languages (POPL) and the Static Analysis Symposium (SAS).
It is our great pleasure to welcome Professor Michael Ernst of the University of Washington, USA as an IMDEA Software Institute visiting faculty member. Michael is an ACM Fellow and author of over 100 publications spanning the spectrum from software engineering, to program analysis (both static and dynamic), to programming language design. His research combines strong theoretical foundations with realistic experimentation, with an eye to changing the way that software developers work.
Deadline: The deadline to submit proposals is July 31st, 2014.
In the last years the need for a more powerful, flexible, and resilient Internet has arisen, not only in the scientific community, but also within its users. The EC has initiated an RTD initiative, the FI-PPP (www.fi-ware.org), which aims at generating new Internet-related technologies and solutions to boost occupation and economy in Europe. This activity intends to establish mutually beneficial links between the FI-PPP and the EIT ICT Labs initiatives.
We expect to select, train, and support up to three start-ups or SMEs dealing with Future Internet and Internet-of-Things technologies. The selection process will be divided into two phases:
The following competences and experience are required:
The SME will take part in the FI-PPP Liaison activity from October 1st to December 31st, 2014. The allocated maximum budget amounts to EUR 25,000.00 per company with room for up to three companies. This shall cover all costs related to the project, including travel costs.
Responses shall include the following information in a maximum of 3 pages:
Please, for more information, contact
The IMDEA Software Institute has been awarded a Marie Curie Career Integration Grant by the People Programme (Marie Curie Actions) of the European Union's Seventh Framework Programme.
The project VeriStab lead by Pavithra Prabhakar will investigate formal verification of stability of embedded control systems. It addresses a very important property in control system design, namely, stability, and proposes novel algorithmic methods to verify stability of large scale embedded control systems. The project will run for a duration of 4 years and will promote the integration of the researcher with the host institute.
The IMDEA Software Institute has published its 2013 Annual Report.
Microsoft Research and the IMDEA Software Institute officially presented their new Joint Research Center.
The collaboration was formalized in late 2013 with the objective of framing and boosting the significant research collaborations between Microsoft Research and the IMDEA Software Institute in software science and technology. The new Joint Research Center sets the ground for a long-term collaboration aiming to advance the science and technology which will allow the cost-effective development of high-quality software products.
Among other relevant members of the public administration, industry, and the software research community, the presentation was chaired by Carles Grau, Public Sector Director at Microsoft Spain; Rocio Albert López-Ibor, General Director for Universities and Research, Regional Ministry for Education; Manuel Hermenegildo, Director of the IMDEA Software Institute; Judith Bishop, Director of Computer Science at Microsoft Research, and Jaime Puente, Director for Latin America at Microsoft Research.
More information at:
The first Workshop of the Joint Research Center between Microsoft Research and the IMDEA Software Institute took place April 2-4, 2014, at the IMDEA Software building in Madrid. The workshop was aimed at reinforcing the collaboration between these two institutions on the following topics:
The Workshop was the launch activity of the Center, at which researchers from both sides worked on topics of joint interest. It was organized by Judith Bishop and Georges Gonthier from Microsoft Research and by Gilles Barthe and Manuel Hermenegildo from the IMDEA Software Institute.
These workshops bring together researchers and students to discuss their collaborative work on hot topics in software in order to advance the state of the art and, where possible, to bring those advances to market. The focus of the first workshop is on verification (coordinated by Alexey Gotsman and Francesco Logozzo), programming languages (coordinated by Pierre Yves Strub and Georges Gonthier), and security (coordinated by Juan Caballero and Ben Livshits).
The 3-day workshop included the following keynote speakers:
Five papers by IMDEA Software Institute researchers have been accepted for publication at the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2014), a top-ranked conference in the area of programming languages and systems.
These five papers are among 51 papers selected for publication out of 220 submissions to the conference.
The president of the Autonomous Region of Madrid, Ignacio González González, presided over the official opening of the building of the Madrid Institute for Advanced Studies in Software Development Technologies (the IMDEA Software Institute), which took place on Monday July 8, 2013, at noon.
The president was accompanied by the Secretary of State for Research, Development, and Innovation of the Ministry for Economy and Competitiveness, Carmen Vela, the Rector of the Technical University of Madrid, Carlos Conde, and the Counselor for Education, Youth, and Sports, Lucía Figar, among other personalities form industry and science and research policy.
With more than 8000 m2, the Institute's new building includes offices, numerous spaces for interaction and collaboration, areas for project meetings and for scientific and industrial conferences and workshops, and powerful communications and computing infrastructures. The layout facilitates the setup of joint research labs with industry and academia. It is highly energy-efficient, through energy-conscious design, co-generation, and full automation.
The Institute is located within the Montegancedo International Campus of Excellence of the Technical University of Madrid, next to the UPM Computer Science department, research centers, and technology transfer facilities, including a company incubator.
The president presented the Institute as one of the instruments that the Madrid Region uses to create an environment that is favorable and confidence-inspiring for companies, that is attractive for innovators, and that helps Madrid boost two of its well-known advantages: its competitiveness and its modernity. Ignacio González concluded thanking everyone for their collaboration in a common project whose goal is to make Spain a country at the forefront, with a sustainable and competitive economy and, especially, to the researchers of the Institute for having selected Spain to develop their talent.European Institute of Innovation and Technology (EIT) ICT Labs (Information and Communication Technologies Labs), the EIT Knowledge and Innovation Community (KIC) in ICT. The goal of EIT ICT Labs is to drive European leadership in ICT innovation for economic growth and quality of life. The decision to admit the IMDEA Software Institute as an associate partner was made by the EIT ICT Labs Steering Committee on March 26, 2013. As the first Spanish EIT ICT Labs member, the IMDEA Software Institute is in charge of coordinating the new associate node (Associate Partner Group) in Spain, which includes as partners the following leading research, development, innovation and business development organizations in Spain: Telefónica, INDRA, Atos, la Technical University of Madrid, and the Barcelona Supercomputing Center. The headquarters (Associate Partner Group Co-Location Center) are located in the new IMDEA Software Institute building. EIT ICT Labs currently has five nodes located in Berlin, Eindhoven, Helsinki, Paris, Stockholm, and Trento, and three associate nodes located in London, Budapest, and now Madrid. The purpose of each node is to catalyze knowledge and innovation development by involving outstanding research institutes, universities, and enterprises from the respective country, following an integrated approach based on a synergy between education, research, and business. Besides ICT Labs, other KICs operating within the EIT framework are concerned with climate and innovative energy solutions.
As part of the activities of the NESSoS Project, the IMDEA Software Institute has organized a one-day training course on the ActionGUI technology, with participation of representatives of ATOS Research & Innovation. IMDEA researchers and ATOS representatives also discussed in depth future extensions of the ActionGUI technology as well as the potential commercial impact of this technology.
Andrea Cerone (postdoctoral researcher at the IMDEA Software Institute) wins the best paper award at the 8th International Federated Conference on Distributed Computing Techniques, for the article Modeling Mac-layer Communications in Wireless Systems. The paper is co-authored by Matthew Hennessy (Trinity College Dublin) and Massimo Merro (Università degli Studi di Verona).
Juan Caballero gives an invited talk at the 38th annual meeting of the Messaging, Malware and Mobile Anti-Abuse Working Group (M3AAWG) in Vienna, Austria. M3AAWG is arguably the most important industry forum dealing with Internet security issues such as bot mitigation, spam, Web messaging abuse, and DNS abuse. The member roster of M3AAWG includes Apple, Google, AT&T, PayPal, Symantec, Time Warner, Facebook, Yahoo, France Telecom, and many other companies. Juan's talk happens on June 6th, and is one of two invited talks from academics in the three day event. His talk deals with the emergence of specialized services in the Malware ecosystem that help attackers monetize Internet-connected computers.
The IMDEA Software Institute has published its 2012 Annual Report.
Within its strategic framework for cooperation with industry, the IMDEA Software Institute has established together with Telefónica Digital, a special Joint Research Unit (JRU) in the area of cloud computing and its supporting infrastructures.
The creation of the JRU kernel started already in December 2012, and it presently includes specialists in the Java and OpenStack platforms, as well as specialists in the administration of virtual cloud resources. The focus of the JRU is on automated definition, deployment, and management of virtual machines, storage, and networks, all of which are the key components for executing cloud applications.
Gilles Barthe has given one of the two plenary Keynote addresses at ETAPS 2013, presenting his work on Computer-aided Cryptographic Proofs, developed at the IMDEA Software Institute. The EasyCrypt tool site provides additional information and references.
The European Joint Conferences on Theory and Practice of Software (ETAPS) is the primary European forum for academic and industrial researchers working on topics relating to Software Science. Established in 1998, it is a confederation of six main annual conferences (CC, ESOP, FASE, FOSSACS, TACAS and POST) accompanied by satellite workshops and other events.
Researchers at the IMDEA Software Institute have 5 papers accepted for publication at the 25th International Conference on Computer Aided Verification (CAV) which is one of the most prestigious conferences in the area of formal methods.
These 5 papers were among the 70 papers selected for publication at CAV out of 209 submission from around the world.
Gilles Barthe, Juan Manuel Crespo, César Kunz, and Mark Marron, IMDEA Software researchers, win the best paper award at The 18th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP'2013), for their article From Relational Verification to SIMD Loop Synthesis.
The paper is co-authored by Sumit Gulwani (Microsoft Research).
The IMDEA Software Institute has been awarded the AutoCrypt project, a joint project with Stanford University, University of Pennsylvania, and SRI. The project is funded by ONR and will run from July 2012 until July 2015.
AutoCrypt aims to use computer technology to provide mathematical guarantees that a cryptographic algorithm is secure, and that it is adequate for a given product, process, or service.
The IMDEA Software team will use EasyCrypt to develop a systematic classification of cryptographic algorithms and to create a cryptographic atlas that will be used by researchers and companies to choose the most suitable algorithm for their needs.
The AMAROUT-II program is now open for
new applications for fellowships. This EU Marie Curie (PEOPLE-COFUND)
program, coordinated by the IMDEA Software Institute, offers 152
fellowships during the next 4 years to experienced researchers to help
develop their individual research projects within any one of the
research institutes comprising the IMDEA network. Each fellowship
funds a researcher for up to three years. The call for applications
will remain open until September, 30 2015, with periodic closing
dates. For more information see AMAROUT-II. Contact:
Alexey Gotsman received the best paper award at The 23rd International Conference on Concurrency Theory (CONCUR 2012). The paper, "Linearizability with Ownership Transfer", was co-authored by Hongseok Yang (Oxford University).
Linearizability is a commonly accepted notion of correctness for libraries of concurrent algorithms. The paper generalizes this notion to the setting of common programming languages, where libraries and their clients can communicate via the heap, transferring the ownership of data structures, and can even run in a shared address space without any memory protection.
The IMDEA Software Institute has been granted the ``ENTRA (Whole-Systems Energy Transparency)'' EU project, which aims to promote the development of greener IT products by enabling "energy-aware" software development. Within the project, starting on October 1, 2012, researchers from the IMDEA Software Institute will create tools for advanced program analysis and modeling of energy consumption in computer systems which will facilitate predictions of energy consumption early in the software design phase. ENTRA is funded by the EU 7th Framework Programme, through the Future and Emerging Technologies (FET) scheme, and has an overall budget of 2.1 million Euro. Apart from the IMDEA Software Institute and Roskilde University, which coordinates the project, the consortium also includes XMOS Ltd. and the University of Bristol.
Local project contact: Pedro López-García
The IMDEA network of institutes has been granted AMAROUT-II, an EU Marie Curie (PEOPLE-COFUND) program that will offer 152 fellowships during the next 4 years to experienced researchers to help develop their individual research projects within any one of the research institutes comprising the IMDEA network. Each fellowship funds a researcher for up to three years. A permanent call for applications will be opened on October, 1 2012 and will run until September, 30 2015, with periodic closing dates. The program, prepared and coordinated by the IMDEA Software Institute, is designed to support transnational mobility of experienced researchers offering attractive working conditions and providing opportunities to deepen and widen their skills. AMAROUT-II is a continuation of AMAROUT, a highly successful COFUND program which is now closed for applications.
For more information see AMAROUT-II. Contact:
The IMDEA Software Institute has published its 2011 Annual Report.
Santiago Zanella, who completed his PhD at the IMDEA Software Institute under the supervision of Prof. Gilles Barthe, is the winner of the 2011 EAPLS Best Dissertation Award for his dissertation "Formal Certification of Game-Based Cryptographic Proofs" defended at the École Nationale Supérieure des Mines de Paris in 2010.
This award is given by the European Association on Programming Languages and Systems to the PhD student who has made the most original and influential contribution to the area of Programming Languages and Systems, and has graduated in the period up to November 2011 at a European academic institute. The purpose of the award is to draw attention to excellent work, to help the career of the student in question, and to promote the research field as a whole.
The winner was selected by a committee of international experts. Details on the procedure can be found here. The candidate theses were judged on originality, impact, relevance, and quality of writing.
With this award already two researchers associated with the IMDEA Software Institute have received this prestigious recognition.
IMDEA Software Institute researchers Alexey Gotsman and Mark Marron each got one of the 10 Microsoft Software Engineering Innovation Foundation (SEIF) Awards given by Microsoft Research in 2012.
Microsoft Research created these Awards to support research in software engineering technologies, tools, practices, and teaching methods. Out of more than 100 applications, only 8 other applicants, in addition to Alexey Gotsman and Mark Marron from the IMDEA Software Institute in Spain, obtained this prestigious award in 2011, 1 in Switzerland, 1 in Canada, and 6 in the United States.
Alexey Gotsman and Mark Marron will be publicly recognized at the new annual SEIF Day, to be held on 18th of July 2012, in Redmond, USA. This event is a new addition to the SEIF program and will be attended by previous and current SEIF winners, influential software engineering researchers, and researchers from Microsoft Research.
The paper Constraint-Based Runtime Prediction of SLA Violations in Service Orchestrations, co-authored by IMDEA Software Institute and UPM Researchers Dragan Ivanovic, Manuel Carro, and Manuel Hermenegildo, was selected as the Best Paper Award at ICSOC 2011, the 9th International Conference on Service Computing held at the Paphos, Cyprus, Dec 5–8, 2011.
The paper presents and evaluates a technique to detect ahead of time whether there will be or not SLA violations in service orchestrations, and to determine under which conditions these will (or will not) happen. The technique uses a model of the process which can evolve as the process executes, thus making it possible to reflect dynamic changes. At every inspection point, the continuation of the process model is sent to the predictor which produces a constraint model by means of symbolic execution using a constraint-generating interpreter. The constraint system is fed into a Prolog-based constraint solver which is, additionally, given boundary conditions to represent scenarios of failure and non-failure. The results of the constraint solver indicate the cases under which these scenarios will or may occur. Evaluations under realistic conditions obtained using the Microsoft Workflow Engine indicate significant prediction capacity with very small numbers of false positives / negatives.
The paper Computer-Aided Security Proofs for the Working Cryptographer, co-authored by IMDEA Software Institute Researchers Gilles Barthe and Santiago Zanella with colleagues at INRIA, is the winner of the Best Paper Award at CRYPTO 2011, the 31st International Cryptology Conference held at the University of California, Santa Barbara, Aug 14–18, 2011.
You can see the presentation at CRYPTO'11 here:
The paper presents EasyCrypt, an automated tool for elaborating security proofs of cryptographic systems which uses off-the-shelf SMT solvers and automated theorem provers. The tool is significantly easier to use than its predecessors and is arguably a plausible candidate for adoption by working cryptographers. The usefulness of the tool is illustrated through its application to security proofs of the Cramer-Shoup and Hashed ElGamal cryptosystems.
The paper Measuring Pay-per-Install: The Commoditization of Malware Distribution, co-authored by IMDEA Software Institute Assistant Professor Juan Caballero, is the winner of an Outstanding Paper Award at the Usenix Security 2011 Symposium.
The paper reports on recent research by Caballero and colleagues from the University of California, Berkeley, suggesting that most malware in personal computers is covertly installed by enterprising hackers, who sell access to the compromised hosts to criminal gangs in an underground Pay-Per-Install (PPI) market. The article was recently the subject of a feature in MIT's Technology review.
Manuel Hermenegildo, Institute Director, was, with Professors Michael Leuschel (University of Düsseldorf) and Antonio Porto (University of Lisbon) part of the winning team of the 18th Prolog Programming Contest at the 27th International Conference on Logic Programming in Lexington, Kentucky, USA. Of course, this was done using Ciao which was duly declared "this year's Prolog system of choice." And all of this while having to endure being continuously referred to by the contest organizers as the "old boys" team...MIT's Techonology review reports recent research by researchers from the IMDEA Software Institute and University of California, Berkeley, suggesting that most malware in personal computers is covertly installed by enterprising hackers, who sell access to the compromised hosts to criminal gangs in an underground Pay-Per-Install (PPI) market.
Pavithra Prabhakar obtained her doctorate in Computer Science from the University of Illinois at Urbana-Champaign in 2011, from where she also obtained a masters in Applied Mathematics. She has a masters degree in Computer Science from the Indian Institute of Science, Bangalore and a bachelors degree from the National Institute of Technology, Warangal, in India.
Pavithra joined the faculty of the IMDEA Software Institute in 2011. She took a one-year leave of absence (August 1 2011 to August 31 2012) at the California Insitute of Technology as a CMI (Center for Mathematics of Information) fellow. She has also spent several summers as an intern at Bell-Labs, Murray Hill, working on formal synthesis of web-services.
She is the recipient of the Sohaib and Sara Abbasi fellowship from UIUC and M.N.S Swamy medal from the Indian Institute of Science.
Her main area of research is in Formal Analysis of Cyber-Physical Systems. She has published widely in Hybrid Systems and Formal Methods conferences and her paper in HSCC has received an honorable mentions award.
The IMDEA Software Institute has published its 2010 Annual Report.
Alexey Gotsman, Assistant Professor at the IMDEA Software Institute, is the winner of the 2010 EAPLS Best Dissertation Award for his dissertation on "Logics and analyses for concurrent heap-manipulating programs" completed at the Computer Laboratory of the University of Cambridge.
This award is given by the European Association on Programming Languages and Systems to the PhD student who has made the most original and influential contribution to the area of Programming Languages and Systems, and has graduated in the period up to November 2010 at a European academic institute. The purpose of the award is to draw attention to excellent work, to help the career of the student in question, and to promote the research field as a whole.
The winner was selected by a committee of international experts. Details on the procedure can be found here. The candidate theses were judged on originality, impact, relevance, and quality of writing. The conclusions from the jury can be found here.
Laurent Mauborgne, Researcher at the IMDEA Software Institute, is one of the winners of the Intelligent Systems Best Paper Award for his article on "Static Analysis and Verification of Aerospace Software by Abstract Interpretation" presented at 2010 AAIA Infotech@Aerospace.
This award is given by the American Institute of Aeronautics and Astronautics.
John Gallagher has been granted a 3-year research project (2011-2013) by the Danish Natural Science Research Council (FNU). The project is entitled "NUSA: Numerical and Symbolic Abstractions for Software Model Checking". NUSA supports collaboration between Roskilde university and the IMDEA Software Institute, and also with Ben-Gurion University, Israel, IRISA/Univ. Rennes, France and K.U. Leuven, Belgium.
The IMDEA Institutes joined the Madrid events of Researchers Night, an EU-wide initiative bringing together the public at large and researchers once a year on the fourth Friday of September. The 2010 edition took place on 24 September in over 600 venues of 250 European cities in 33 countries. In Madrid there were several activities, including a round table with all the directors of the IMDEA Institutes.
Juan Caballero (Ph.D Carnegie Mellon University) has joined IMDEA Software as an Assistant Research Professor (tenure-track). Before joining IMDEA, he was Visiting Graduate Student at UC Berkeley.
The Counselor for Education of the Madrid Regional Government, Lucía Figar, visits the construction site of the building that will be the permanent location of the IMDEA Software Institute. Press release. Pictures.
Alexey Gotsman (Ph.D. University of Cambridge, 2009) has joined IMDEA Software as an Assistant Research Professor (tenure-track). He previously held a postdoctoral researcher position at the University of Cambridge, where he also obtained his Ph.D.
The IMDEA Software Institute has published its 2008-09 biennial report.
IMDEA Software has organized the ES_PASS Project Workshop on "Industrialization of Abstract Interpretation," held on October 28, 2009 in Madrid (Spain), a succesful experience where the results of the ES_PASS project have been presented to a wide and varied audience of mostly industrial and also some academic participants, and where new contacts and synergies among such participants have been established.
ES_PASS (Embedded Software Product-based Assurance) is an EU ITEA2 project that aims at improving and integrating state-of-the-art software verification techniques based on static analysis into existing industrial engineering processes in the domain of safety-critical embedded systems.
The project consortium includes industrial participants such as Airbus France, AbsInt, CS Systèmes d'Information, Continental Automotive France SAS, Thales Avionics, Daimler AG, Esterel Technologies, PSA Peugeot Citroen, Siemens VDO Automotive, EADS Astrium, GTD Barcelona, Onera, PolySpace Technologies, Thales Transportation, ALCATEL TSD and IFB Berlin, as well as a number of research laboratories and institutes.
Local project coordination and workshop organization: Pedro López-García.
Laurent Mauborgne has joined the Institute in a Researcher position. Laurent was previously assistant professor at École normale superieure and part-time professor at École polytechnique, France. He received his Ph.D. in Computer Science from École Polytechnique, in 1999, and an habilitation à diriger les recherches from University Paris-Dauphine (France) in 2007. His research focuses on static analysis of programs and abstract interpretation. The goal is to develop theoretical as well as practical tools to analyze the behaviors of programs. He is one of the authors of the Astrée analyzer, a tool that proves the absence of run-time errors in critical avionic code.
John Gallagher (jointly with Henning Christiansen) wins the Best Paper Award at the International Conference on Logic Programming 2009 in Pasadena, CA, USA, for the paper "Non-Discriminating Arguments and Their Uses". The award is given by the Association for Logic Programming.
Gilles Barthe, Manuel Hermenegildo, and Manuel Clavel attended the HATS kick-off meeting, held in Bologna, Italy, on March 9-11, 2009. HATS is a recently approved FP7 IP project which focuses on the rigorous development of software product families (SWPF). The technical core of the project is an Abstract Behavioral Specification language which will allow precise description of SWPF features and components and their instances. IMDEA Software is part of the HATS consortium, in collaboration with UPM, along with 7 other academic partners, 2 research institutes, and 1 SME.
The IMDEA Institutes network granted a 7FP (PEOPLE-COFUND) Marie-Curie Action for researcher mobility. The program, called AMAROUT, co-finances for one year (renewable for two or three) the integration of more than 130 researchers in the IMDEA network of institutes. The duration of the AMAROUT program is 4 years, beginning on March 1st, 2009. IMDEA Software is the proposer and coordinator of the AMAROUT program.
Building designs from six renowned architects were received in response to our call for design ideas for a new building to be the permanent location of the Institute. In november 2008 a committee formed by members of IMDEA Software, the Madrid Regional Government, and external experts chose the winning design, presented by Estudio Lamela. Construction of this new building will begin shortly and will be ready when the Institute outgrows its current temporary location in a floor of the UPM CS Department.