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.
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.