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 machine code. It has also been improved, extended, and generalized in several ways over the last 10 years.
The content of the paper and a summary of its impact in other work in this decade will be presented in a plenary invited talk at the ICLP 2017 conference, which will be held in Melbourne, Australia, from August 28 to September 1, 2017, co-located with SAT'2017 and CP'2017.
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.
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. Cesar Sanchez) 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 Cesar Sanchez 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 Cesar Sanchez 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 Max Planck Institute for Software Systems, Germany. 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 Ivanović, 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.