IMDEA Software and IMDEA Networks Institutes participate together with six other partners (Instituto Nacional de Técnica Aeroespacial, Centro Español de Metrología, Fundación Vithas, Universidad Autónoma de Madrid, Universidad Politécnica de Madrid and Universidad Complutense de Madrid) in the MADQuantum-CM project, funded by the Madrid Regional Government, the Spanish State through the Plan for Recovery, Transformation and Resilience, and the European Union through the NextGeneration EU funds. The objective of the project is the expansion of MadQCI, the new quantum communications network of the Madrid Region and the largest quantum network in Europe.
Quantum computing and quantum communications have the potential to become a paradigm shift in computer networks. In this sense, MadQCI will connect, through a metropolitan fiber optic deployment, data centers of the universities of the Madrid Regional Government and the IMDEA Software and IMDEA Networks Institutes. The network will allow the permanent hosting of quantum communications equipment, enabling the validation of new key exchange technologies, as well as the development of use cases and innovations that take advantage of the infrastructure, which will be deployed by REDIMadrid, the advanced data network of the Madrid Region, managed by IMDEA Software.
"Quantum key exchange technology has a very large disruptive potential, as it guarantees key exchange and consequently secure communications between remote centers," explains César Sánchez, director of REDIMadrid, Senior Researcher at IMDEA Software and principal investigator at IMDEA Software on the project. "Europe has a world leadership in quantum technologies, and in the coming years we will see many academic as well as industrial advances in quantum communications," he continues.
"This technology will not only improve the performance and capacity of networks, but will change the very foundations, completely changing computing platforms," as Albert Banchs, Deputy Director of IMDEA Networks and principal investigator of the project at IMDEA Networks, explains. Furthermore, "quantum communications will be beneficial, from a social point of view, as they help to create highly sensitive data transmission networks based on a process called quantum key distribution, or QKD, which takes advantage of the laws of quantum physics to protect data. This technology is already used, for example, by financial institutions, but extending it to other areas would require major innovations. The project will also help to foster the development of new local quantum technology companies," says Ignacio Berberana, Senior Research Engineer at IMDEA Networks and a participant in the project together with the Institute's Edge and Global Computing research groups.
MADQuantum-CM aims to show how quantum security solutions can be used throughout the scientific network infrastructure of the Madrid Regional Government in a transparent manner. Among its aims is also to create several testbeds and demonstrations to show how quantum networks and communications can be used by potential stakeholders. As Berberana points out, two of the areas to be explored in this project will be the application of quantum cryptography and quantum communications to support new networks, such as the future 6G networks.
In addition, it seeks to develop an innovation and training ecosystem to help grow the technology and supply chains for quantum communications technologies and services in Madrid and Spain (through collaboration with other regional quantum communications projects). The network infrastructure deployed by the project is expected to form the basis of a permanent quantum network that will enable continued innovation beyond its lifetime. Ultimately, these projects build on the extensive quantum communications expertise of their participants.
"In the case of IMDEA Software, its participation in the European OpenQKD project, which culminated at the beginning of 2023, made it possible to build on the REDIMadrid network the largest European quantum communications testbed, the germ of the current MadQCI network", highlights Sánchez. "In the case of IMDEA Networks, the project is based on the results of the European 5G Vinni and OpenQKD projects," says Berberana.
The Madrid Community Complementary Quantum Communications Plan (MADQuantum-CM) is funded by the Madrid Regional Government and MCIN with NextGenerationEU funds from the European Union's Recovery and Resilience Mechanism (RRM), in the framework of the Recovery, Transformation and Resilience Plan of the Spanish State (PRTR-C17.I1).
Researcher Konstantinos Papaioannou, PhD Student of the IMDEA Software Institute (advised by Thaleia Dimitra Doudali), won the Distinguished Artifact Evaluator Award at the 2023 European Conference on Computer Systems (EuroSys 2023) for his exceptional service in the Artifact Evaluation Committee of the conference.
EuroSys is a premier conference on various aspects of systems software research and development, including its ramifications for hardware and applications. Topics of interest for the conference include: operating systems, database systems, real-time systems, networked systems, storage systems, middleware, distributed, parallel, and embedded computing systems.
EuroSys 2023 has been a five-day event. The first day is devoted to workshops, to allow junior and senior researchers to interact in a friendly environment on cutting-edge ideas. The other four days are dedicated to the main conference track.
IMDEA Software Institute hosted at his headquarters the workshop on model-based engineering and its applications. The workshop brought together experts from different branches of research within Model-Driven Engineering (MDE) to discuss their techniques, advances and applications to different domains. The event, organized by the post-doctoral researcher of the IMDEA Software Institute Fernando Macías, was a great success and succeeded in sharing knowledge through the proposed talks.
It lasted the whole day, starting with the opening by Fernando Macías, and leading to the first talk, in which Cristina Vicente, from University of Extremadura gave an introduction to the design of container-based applications or educational robots, up to the management of fleets of autonomous self-adaptive robots.
The second talk was given by Roberto Rodríguez, also from University of Extremadura who discussed a model-based framework for the definition of data science pipelines independent of the particular execution platform and tools that alleviate problems such as the execution of pipelines in different environments.
After a coffee break, the next talk was given by Volker Stolz, from Western Norway University of Applied Sciences, who presented a modeling for smart home interoperability and how to represent it in one of the standards for IoT, SAREF, as well as the challenges involved. The goal is to achieve its use for migration between different smart home platforms.
Violet Ka I Pun, also from Western Norway University of Applied Sciences presents the preliminary results of the CROFLOW project, focused on decision making to optimize workflows. The goal is to automate these processes and make them less manual and more efficient.
After a lunch break, José Ignacio Requeno from Universidad Complutense de Madrid, resumed the talks by presenting Petri Nets (PN) -an automata-based formalism for modeling concurrent systems- for MDE.
Next, Adrian Rutle of Western Norway University of Applied Sciences spoke about multi-modeling, alluding to various ways to achieve coherence and also presented an approach to restoring coherence based on reinforcement learning.
Subsequently, Pablo Parra from Universidad de Alcalá de Henares described the model-based solutions adopted to facilitate the development of on-board software on satellites within the project for the development of the instrument control unit of the Energetic Particle Detector of the Solar Orbiter mission, among others.
To conclude the event and as the last talk, Óscar Rodríguez from UAH based his presentation on the application of modeling techniques for on-board satellite applications, such as requirements management and design, validation and verification activities.
The Institute IMDEA Software researcher, Miguel Morona, was awarded with the second "Leonardo Torres Quevedo" prize in the specialty of Cryptology and Information Security, sponsored by CSIC and ITEFI, on March 28th, 2023. This distinction has been achieved thanks to his final degree work: "Algebraic Constraint Systems for Cryptographic Proofs applied to SHA-256", which is the basis for the demonstration and verification of the hash code through matrices.
SHA-256 is a function based on an algorithm commonly used in cryptography for data compression, especially applied for digital signatures. Its widespread use is mainly due to its ability to effectively ensure data integrity, associating a unique 64-digit identifier to each text. Its applications are unlimited, allowing to detect any modification in the data since, in that case, the hash code will be radically different from the original one.
IMDEA Software researchers, Dario Fiore and Ignacio Cascudo, have supported and advised Miguel's work, in which he manages to obtain an optimal R1CS (Rank 1 Constraint System) in terms of the algebraic relations of SHA-256, taking into account the generation of matrices with 23296 rows and 26113 columns. This algorithm guarantees that the hash code is correct and verifies it through the matrices.
This represents an evolution in cryptographic proofs, as it allows them to be more efficient.
Aleks Nanevski has dedicated his life to solving one of the biggest computer science challenges, taking a long and risky road towards revolutionizing how we think about programming in general, and concurrent programming specifically.
IMDEA Software Institute researcher Aleks Nanevski was awarded an ERC grant for "MATHADOR: Type and Proof Structures for Concurrent Software Verification in April 2017 worth €2 million. The project, funded by the European Union’s Horizon 2020 program, has lasted 6 years and ended on March 31st. His research, as the European Research Council indicated at the time of the grant award, is high-risk because it proposes new foundations for concurrent software verification, but it is also high-gain, since concurrent software verification is one of the most important open problem in current research on programming languages and semantics.
Enter functional programming and type theory; centered in the academic world, these subjects have roots in philosophy, logic, and constructive mathematics. Functional programs may not be as fast to execute as imperative programs---the ones used by software industry---but they are much easier to write and understand. An imperative program with hundreds of lines of code can often be reduced to just a few lines in the functional idiom. When programming imperatively, we adapt to the machines. When programming functionally, we have the machines adapt to us. The idea of functional programming is to use a mathematical language that is so minimalist, concise and effective that it makes it easy to spot the programming errors, and thus not even make errors in the first place.
Aleks explains that his research is related to "Everything and nothing at the same time. It is a foundational problem, which implies that it is highly idealized. It takes its challenges from existing practices and technologies and removes the messiness of the real world, while striving to distill the basic core issue. That makes it related to nothing directly. But it also makes it related to everything, because that core issue is what it means for programs to interact and coordinate with each other, and this interaction arises in Artificial Intelligence, in Internet of Things, and everywhere in-between. Because of its universality, understanding the issue mathematically will open possibilities for the technologies of the future that today we can't even imagine."
"I started with an intuition that concurrency should fruitfully be addressed by functional programming and type theory, because I applied these previously to non-concurrent programming, which uncovered deep connections with so-called Separation Logic, an important and well-known idea in computer science. Somewhat amazingly, this intuition has so far always materialized, even when it temporarily looked like it has no chance. However, there is still a long way to the top.", according to Nanevski.
“This project has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (Grant agreement No. [724464])”
PhD student, Martín Ceresa, visitor at IMDEA Software Institute, has defended his thesis at the National University of Rosario on April 5th, entitled: "Theory of Improvements with Effects", directed by Dr. Mauro Javier Jaskelioff.
Optimizing programs is not an easy task. A transformation does not necessarily imply an improvement. Therefore, when modifying a program, it must be shown that the semantics of the program are preserved, and furthermore, it must be ensured that the transformation is really an optimization, that the execution of the program is improved.
Martin's thesis shows that there are several possible interpretations for the programs, but not all of them allow the natural introduction of intensive properties of their execution. This separation between the interpretation of programs and their evaluation leads him to implement program evaluation in order to have information relevant to resource consumption.
Functional languages have clearer semantics than non-functional languages. Knowing this fact has allowed him to perform equivalence tests of programs, but they hide properties of the execution. This has been the main motivation in the research world for the development of improvement theories and Ceresa has been able to present for the first time a relational theory of functional program costs.
Martin successfully characterizes improvement theories for functional languages with algebraic effects. "On the one hand, we add more expressiveness to functional languages by introducing algebraic effects, a subset of computational effects. While on the other, following the literature, we identify the definition of inter-program enhancements as a refinement of observational equivalence."
Ceresa concludes that the thesis raises the beginning of the research of the study of intensive property analysis on functional language with algebraic effects opening more questions than solutions, which gives rise to a long-term future in the field of research in this regard.
IMDEA Software has participated once again with the rest of IMDEAs in the Madrid is Science Fair, organized by the Fundación para el Conocimiento Madrimasd, which took place from March 23rd to 25th.
The Madrid is Science Fair is a science outreach event aimed at school communities and the general public. Madrid is Science is conceived as a comprehensive showcase of the R&D&I capabilities of the Madrid Regional Government for the construction of a sustainable future, showing citizens the response that Science, Technology and Innovation can give to the challenges of the planet.
IMDEA Software led various activities for the public at the Fair to play and understand some computer science concepts. They were able to learn how an algorithm works by playing "The Towers of Hanoi"; to decipher and encrypt code with "Caesar's disks"; what an image is for a computer through "Instagram filters"; how to speed up tasks with parallelism using sums and/or cards from a deck of cards; circumvent the security controls of a server with "HacKtivity"; and search and describe secure protocols without revealing secrets through "Multi-Party Computation", among others.
23rd of March
Researchers Diego Castejón, Srdjan Matic, Konstantinos Papaioannou and Georgia Christofidi attended the visitors during the first day.
The director of IMDEA Software, Manuel Carro, attended the official opening of the Fair and visited the stand together with the Vice-Minister of Universities, Science and Innovation; Fidel Rodríguez Batalla, the General Director of Universities and Higher Artistic Education of the Madrid Regional Government; Ricardo Díaz, and the president of the Madrimasd Foundation; Federico Morán. Carro introduced them to Multi-Party Computation and Diego Castejón was in charge of guiding them to follow a protocol through a game of cards and numbers.
24th of March
On the second day, researchers Fernando Macías, Marcos Grandury, Daniela Ferreiro, Niki Vazou, Juand Caballero, Pedro Moreno and Martín Ceresa were at the stand.
The Vice President and Councilor for Education and Universities, Enrique Ossorio, Fidel Rodríquez Batalla, Ricardo Díaz and Federico Morán visited the IMDEA stand after the official visit to the Aula Fair. The General Director of Research and Technological Innovation, Ana Isabel Cremades, also stopped by IMDEA's stand in the afternoon.
After the official visit, science popularizer Javier Santaolla presented the AMAUTAS platform and the collaboration agreement between the IMDEA Institutes and the scientific knowledge platform. Santaolalla was assisted by IMDEA Materials researcher Mónica Echeverry for the presentation, as she is the protagonist of the first course resulting from this collaboration: "Materials that save lives", which is now available at AMAUTAS.
25th of March
IMDEA Software's Director, Manuel Carro, Martín Ceresa, David Balbás, Gabina Bianchi and Louis Rustenholz were in charge of the stand during the third and last day, where families and people of all ages were able to learn first-hand what the Institute does.
IMDEA Software sponsored and collaborated in the organization and preparation of problems for the [AdaByron Madrid] contest (https://ada-byron.es/2023/reg/madrid/), which was held at the Computer Science School of the Universidad Politécnica de Madrid on March 10 and 11, 2023.
The AdaByron Madrid regional competition is a university competition aimed at students from Madrid universities in which their programming skills and abilities are measured. One of the objectives of the competition is to encourage computer science students to participate in the International Collegiate Programming Competition (ICPC). The winners of the local competition will participate in the national competition, which will be held in Madrid in May, along with the top finishers from the rest of the Spanish regions.
This year, the Institute has actively participated in this event, being a great opportunity to show talented students what IMDEA Software is and what it does.
In addition to IMDEA Software, the Madrid regional AdaByron was sponsored by Accenture and INETUM.
Manuel Carro, Director of the Institute, Juan Céspedes, Network and Systems Engineer, and Margarita Capretto, PhD student, collaborated in preparing the problems to be solved and judging them. Carro also gave an inspirational talk during the seconf day about the Institute and encouraged the students to work for IMDEA Software.
The team "Los Caraduras", formed by David Andrés López Gómez, Ignacio Castellano Vega and Flavius Abel Ciapsa, from the Universidad Complutense de Madrid, was the winner of the IMDEA Software prize which consisted of a Soundcore Space Q45 wireless headset for each team member. The criteria for the award was that the winner would be the one who solved the most problems proposed by IMDEA Software. Since there was a tie, the tie was broken by choosing the team that solved the problems in the shortest time.
IMDEA Institutes are participating in the third edition of the City and Science Biennial in Madrid from February 21-26, 2023. An event organized in collaboration with the Círculo de Bellas Artes and promoted by the Spanish Foundation for Science and Technology (FECYT).
IMDEA Software Institute researchers shared space with IMDEA Energy on Thursday, February 23, and welcomed hundreds of students of various ages, teachers and families.
Martin Ceresa (PhD student) and Gabina Bianchi (intern student), in charge of the IMDEA Software booth, explained to everyone who came by the stand the games related to computer science that were brought and also what they are used for in practice.
People of all ages were able to play to Hanoi Towers and learn about algorithms and information transfer in databases; decipher code using Caesar disks; and perform large sums using parallelization.
The IMDEA Software Institute participates one more year together with the rest of IMDEAs in Transfiere, which has been held from Wednesday 15th to Friday 17th of February at the Congress and Fair Palace of Málaga (FYCMA) .
Transfiere is the main R&D&I meeting point in Southern Europe for sharing scientific and technological knowledge, promoting innovation and connecting science and business. It is a key professional and multisectorial forum for the transfer of knowledge, the improvement of competitiveness in the business sector and the generation of business and networking opportunities.
As in previous editions, the innovation space of the Madrid Regional Government was made up of stands from the IMDEA Institutes and the OTRIs.
Juan José Collazo, Project Manager of IMDEA Software, attended on behalf of the Institute and shared space with colleagues from other IMDEA centers whose objective was to generate synergies with companies to make possible the technology transfer of the research carried out at the Institute.
The auditorium of the School of Computer Engineering (ETSIINF) of the Universidad Politécnica de Madrid hosted the event "Innovating in Feminine: Women in Montegancedo", on the occasion of the International Day of Women and Girls in Science. A meeting organized by IMDEA Software, CeDInt, E-USOC, CBGP, IDR and CTB, research centers of the UPM Montegancedo Campus.
The day began with a round table discussion moderated by ETSIINF professor Clara Benac, with the participation of Silvia Sebastián (IMDEA Software), Elena Ramírez Parra (CBGP), Noelia Blázquez García (Cedint) Master Student, Montserrat Bayón Laguna (IDR), Úrsula Andrea Martínez Álvarez (E-USOC) and Ana López Hernández (CTB).
This was followed by the workshop "Climate Change: Plants fight back" with the participation of Patricia Fernández Calvo from CBGP - Ramón y Cajal CSIC. This was continued by the workshop "Sensorizing realities" given by María José García Cabrera and Noelia Blázquez García from CEDINT.
After a short break, the workshop "Playing with Artificial Intelligence" took place, in which researchers Thaleia Dimitra Doudali, Georgia Christofidi and Margarita Capretto, from IMDEA Software, explained how Artificial Intelligence works, what it is used for, future applications and answered questions from the audience.
"UPMSat: From university to space" was the next workshop given by Elena Roibás Millán and Montserrat Bayón Laguna from IDR. This was followed by the CTB workshop: "Understanding the basic unit of life: Cell cultures". And finally the E-USOC closed the event with the workshop: "Space science: experiments in microgravity".
Last January 30 and 31 the IMDEA Software Institute hosted the hibrid kick-off meeting of the European project "Confidential6G".
The project will will base its research on three pillars: post-quantum cryptography, confidential computing and confidential communication. In short, confidential computing and privacy-preserving technologies for 6G.
The Confidential6G project has a consortium composed of 13 entities from Greece, Spain, France, Germany, the Netherlands, Serbia, Finland, Austria and Ireland. The Spanish participation is represented by the IMDEA Software Institute and the company Telefónica Research and Development.
The consortium will develop the project from January 2023 to December 2025, and will have a budget of 5,263,864 euros, of which 4,999,153 euros are financed by the European Commission's Horizon Europe research program.
ACM, the Association for Computing Machinery, has named 57 of its members ACM Fellows -a list, which includes Manuel Hermenegildo-, for wide-ranging and fundamental contributions in a large number of areas within Computer Science.
ACM is the world's largest educational and scientific computing society, uniting educators, researchers, and professionals to inspire dialogue, share resources, and address the field's challenges.
The ACM Fellows program, initiated in 1993 among leaders in the field of Computer Science, recognizes the top 1% of ACM Members for their outstanding accomplishments in computing and information technology and/or outstanding service to ACM and the larger computing community. Fellows are nominated by their peers, with nominations reviewed by a distinguished selection committee.
In keeping with ACM’s global reach, the 2022 Fellows represent universities, corporations, and research centers in Canada, Chile, China, France, Germany, Israel, the Netherlands, Spain, Switzerland, and the United States.
Manuel Hermenegilgo, Distinguished Professor of the IMDEA Software Institute, has been elected for his contributions to program analysis, verification, parallelism, logic programming, and to the IMDEA Software Institute.
The OPENQKD project culminates after three years of duration and a budget of 15 million euros financed by the European program Horizon Europe 2020. The consortium, which is made up of 38 members, 4 of them Spanish, has installed a test quantum communication infrastructure in several European countries.
Institute IMDEA Software has participated in the OPENQKD project, through REDIMadrid, by providing the physical infrastructure and personnel expertise.
Classical and quantum communications will in the near future jointly secure the ICT needs of European governments, service industries (e.g. healthcare, finance), businesses and citizens, even in the presence of quantum computers or other sophisticated algorithmic attacks against public key infrastructures.
The project culminates having accomplished its mission, establishing secure communication based on QKD and making the technology robust and reliable.
REDIMadrid has managed to deploy a research network on its own infrastructure, thus avoiding a contracted capacity network, with new dark fiber laid and used exclusively for research activities.
In this context, REDIMadrid has made it possible for quantum lambdas to coexist with research traffic lambdas, so it has been possible to test how the solution works in a real environment.
This project has received funding from the European Union's Horizon 2020 research and innovation program under grant agreement no. 857156.
Madrid was the city chosen to hold the last QKD meeting of the European quantum communications project, OpenQKD, which took place from Tuesday 13th to Thursday 15th December.
The event was attended by representatives of the 38 members of the OpenQKD consortium, including REDIMadrid, as well as companies and academics from the national territory.
On Tuesday, December 13th, the OpenQKD General Assembly was held at the "E.T.S.I de Minas y Energía" of the Universidad Politécnica de Madrid (UPM), where internal issues of the project were discussed and decisions were taken in view of the closing of the project in March 2023.
The "QKD Days 2022", organized by AIT (Austrian Institute of Technology), UPM and Telefónica, and promoted by OPENQKD, were held on Wednesday 14th and Thursday 15th December. The QKD Days 2022 focused on the EuroQCI project, which will implement a Europe-wide quantum network.
Wednesday's conference: "On the Road Large QKD Networks in Europe" was held at the "E.T.S.I de Minas y Energía" of UPM. Experiences and knowledge acquired during the OpenQKD project were shared and the future structure of the EuroQCI network was also presented.
Vicente Martín, Professor at the ETSIINF of the UPM, presented the project of the future Madrid Quantum Network of which the IMDEA Software Institute will be part through REDIMadrid. "The evolution of this network together with the future regional networks of Castilla y León, Basque Country, Galicia and Catalonia will allow the integration of the Madrid Quantum Network with the rest of the EuroQCI quantum network" said Martín.
Round tables were also held to discuss how to implement these future networks. As a final point, presentations were made by QKD equipment manufacturers on what are the current devices and what is their vision on the implementation of the devices.
Thursday, dedicated exclusively to "Industry Days", was held at the E.T.S.I de Industriales of the UPM. Industry offered its vision on future quantum networks and their evolution. And the companies that will be final consumers of these networks shared in this conference what they expect from them for industrial use.
IMDEA Software researchers Gibran Gómez, Pedro Moreno-Sánchez and Juan Caballero have created an open-source automated tool to track the financial relationships of malicious entities that abuse Bitcoin technology, tested on 30 malware families. The study "Watch Your Back: Identifying Cybercrime Financial Relationships in Bitcoin through Back-and-Forth Exploration", in which they present their research and the tool, was presented at the prestigious CCS'22 conference (ACM Conference on Computer and Communications Security) last November.
Cybercrime is the plague of the digital environment. Scams, phishing, identity theft, personal data theft, phishing or computer fraud are just a few examples of illicit activities on the network. Blockchain technology and cryptocurrencies, such as Bitcoin, have consistently attracted the attention of cybercriminals, who have frequently used them as a means of payment and even as a means of storing data for illicit purposes.
Aware of this problem, Gibran, Pedro and Juan have analyzed more than 7,500 Bitcoin addresses belonging to 30 malware families, including ransomware families, clippers, sextorsion, crypto-hackers or info stealers.
The main advantage provided by the back-and-forth exploration method, used in the study, is that it allows tracking all transactions produced by a Bitcoin address recursively. This means that, if a Bitcoin address receives cryptocurrencies from another address, and this in turn sends them to a third address, the complete path of the cryptocurrencies could be traced starting from the first address, or from the last one.
As Gibran Gómez points out, "one of the main advantages of the tool is that the user can replicate the whole process in a transparent way, which allows the results to be corroborated".
The tool, in addition to serving Bitcoin users themselves, could be especially useful for law enforcement agencies, as it would allow them to identify routes between malicious addresses and deposit addresses belonging to financial entities regulated by KYC policies, such as exchanges (cryptocurrency exchanges), and which are used by operators of illicit activities. This means that the National Police, for example, could use such routes as evidence to obtain a court order to require from an exchange the personal identification data associated with the addresses involved, and get to know who the final recipients of the money obtained fraudulently are.
In addition, Gómez advises users to take certain precautionary measures before carrying out transactions to avoid being the target of cybercrime: "Paying close attention when including the destination address in a transaction is essential. It is necessary to check several times that the destination address is correct to avoid clippers". To prevent malware, he suggests always using antivirus software and running frequent computer scans and, lastly, performing constant back-ups to avoid the loss of important data that can result from a ransomware attack.
Isabel García-Contreras (currently at the University of Waterloo, in Canada), a former PhD student at the IMDEA Software Institute and UPM's ETSIINF School of Computer Science, under the supervision of Manuel Hermenegildo and José Francisco Morales, has been awarded one of UPM's best PhD thesis awards for the 2020/2021 academic year for her thesis: "A scalable static analysis framework for reliable program development exploiting incrementality and modularity," defended in July of 2021. There were only two such awards for theses defended at the School of Computer Science in this period.
On November 17th, the IMDEA Software Institute held the "Communication: practical course for researchers" given by The Conversation, which was attended by a total of 40 participants.
For the Institute, science communication educates society, provides recognition, helps to achieve media relevance and paves the way for knowledge transfer to companies and society in general.
However, it is not always easy for a researcher to go from writing scientific articles to communicating science to the general public. It is necessary to acquire tools that can help them in the process in addition to receiving support from the communication department.
The course was divided into five modules that were taught by experts in each subject:
Module 1: "How to write a scientific article for media" Claudia Lorenzo. Module 2: "What captures the reader's attention?" Elena Sanz Module 3: "How to face an interview in press, radio or television" Alicia Gonzalez Module 4: "Case study: testimony of a scientist" Alberto Nájera Module 5: "Presence in social networks: The importance and how to manage them" Patricia Ruiz
During the course, it was announced that the IMDEA Software Institute is collaborating with The Conversation so that its researchers can write scientific articles on its platform directed to the media and general public.
50 students from IES Francisco Umbral (Ciempozuelos) and IES Liceo San Pablo took part in the "Gymkhana: Software Matters", organized by the IMDEA Software Institute on the occasion of the XXII Science and Innovation Week, organized by the Madrid Regional Government in collaboration with the Foundation Madrimasd.
The director of the Institute, Manuel Carro, began talking to students and teachers about the research carried out at the institute and the importance of software. "If software stops working, everything stops: mobile phones, lights, modern cars, electricity... Without software we wouldn't have the world we have today", spotted Carro.
Blanca Gutiérrez, Communication Manager of the Institute, presented the activity and gave the fundamental guidelines to the 15 to 17 year old students.
Students were divided into five groups and they had to follow a map to get to the five challenges of the Gymkahana. Each of the challenges addressed software-related topics such as: artificial intelligence, concurrency, parallel sums, program analysis and verification, and cryptography.
They had 13 minutes to solve each challenge where David Balbás, Diego Castejón, Martin Ceresa, Louis Rustenholz, Claudia Bartoli, Juan Manuel Copia, Daniel Jurjo, Laura Herrero, and Fernando Macías as challenge managers explained explained to them everything they required to solve the games as a team.
Once the "Gymkhana: Software Matters" was over, the groups met in the Lecture Hall, where the researchers tallied the scores until the winning team was discovered. Finally, prizes were awarded to the ten members of the winning team, from IES Francisco Umbral.
A bunch of IMDEA Software researchers attended the ACM Conference on Computer and Communications Security (CCS) in Los Ángeles, from November 7-11, to present the 8 papers that were accepted.
ACM is the flagship annual conference of the Special Interest Group on Security, Audit and Control (SIGSAC) of the Association for Computing Machinery (ACM). The conference brings together information security researchers, practitioners, developers, and users from all over the world to explore cutting-edge ideas and results.
In addition to the achievement of having published 8 papers, there are others: Marco Guarnieri's paper "Automatic Detection of Speculative Execution Combinations" obtained a distinguished paper award and researchers Juan Caballero and Dario Fiore received a best reviewer award.
List of the accepted papers.
1. Automatic Detection of Speculative Execution Combinations (Xaver Fabian, Marco Guarnieri, Marco Patrignani)
2. Efficient Zero-Knowledge Proofs on Signed Data with Applications to Verifiable Computation on Data Streams (Dario Fiore, Ida Tucker)
3. Foundations of Coin Mixing Services (Noemi Glaeser, Matteo Maffei, Giulio Malavolta, Pedro Moreno-Sanchez, Erkan Tairi, Sri Aravinda Krishnan Thyagarajan)
4. Watch Your Back: Identifying Cybercrime Financial Relationships in Bitcoin through Back-and-Forth Exploration (Gibran Gomez, Pedro Moreno-Sanchez, Juan Caballero)
5. Enforcing Fine-grained Constant-time Policies (Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya)
6. Sleepy Channels: Bi-directional Payment Channels without Watchtowers (Lukas Aumayr, Sri Aravinda Krishnan Thyagarajan, Giulio Malavolta, Pedro Moreno-Sanchez, Matteo Maffei)
7. Tidy: Symbolic Verification of Timed Cryptographic Protocols (Gilles Barthe, Ugo Dal Lago, Giulio Malavolta, Itsaka Rakotonirina)
8.Succinct Zero-Knowledge Batch Proofs for Set Accumulators (Matteo Campanelli, Dario Fiore, Semin Han, Jihye Kim, Dimitris Kolonelos, Hyunok Oh)
IMDEA Researchers Manuel Hermenegildo, John Gallagher, and José Francisco Morales participated in the Prolog Day Symposium held on November 10, 2022 in Paris.
Manuel Hermenegildo gave the keynote address on "50 years of Prolog and Beyond" and participated in the panel for the first session on "What is Prolog and why is it important?", chaired by Robert Kowalski. He also chaired the session on the Alain Colmerauer Prize and made the Announcement of the Prize winner. José Francisco Morales participated in the panel on "Prolog Thinking and Education", and John Gallagher participated in the panel on "Prolog-powered applications", chaired by David S. Warren.
The Prolog Day Symposium presented the highlights of the Year of Prolog, celebrating the 50th anniversary of the birth of the Prolog programming language. There were more than 230 registered participants, both in-person at the auditorium and on line. It was broadcast online and recorded.
The Symposium included several sessions with presentations and round tables and the awarding of the inaugural edition of the ALP Alain Colmerauer Prolog Heritage Prize for recent practical accomplishments that highlight the benefits of Prolog-inspired computing for the future.
The morning was devoted to the nature and importance of Prolog, Prolog thinking, and Prolog education. The afternoon was devoted to the applications of Prolog, including also the session devoted to the Alain Colmerauer prize, with presentations of the Prolog applications selected as the five finalists for the prize. This was followed by the awarding of the prize.
The IMDEA Software Institute has participated in the first edition of P4i – Patents for Innovation, an event that aims to become the largest European meeting point for Innovation and Technology Transfer. More than 360 patents were shown and P4i counted with over a thousand attendees and exhibitors. Blanca Gutiérrez, Communications Manager of IMDEA Software, represented the Institute from the innovation space of the Madrid Regional Government in La Nave (Madrid), from October 26 to 27.
P4I 2022 was born as a forum for technological innovation and also as a patent fair, thus allowing the creation of a market for the transfer of research results and the purchase and sale of scientific patents. It was attended by 100 universities and research centers, European consortiums such as CIVIS, 110 companies interested in science, investment groups, or companies dedicated to patent drafting.
The welcoming ceremony was led by Fidel Rodríguez Batalla, Deputy Regional Minister for Universities, Science and Innovation of the Regional Government of Madrid, Amaya Mendikoetxea Pelayo, Rector of the Universidad Autónoma de Madrid (UAM), and Félix Zamora, Vice Rector for Transfer, Innovation, and Culture of the UAM.
According to the Vice Rector, "the commercialization of research carried out in universities and research centers is something that should be common for all the entities for the society's improvement".
As for Rodríguez Batalla, the Madrid Regional Government is working to enhance and make available to society the research carried out in universities, research centers such as the IMDEA Institutes and business R&D, "because without science there is no future and no prosperity" pointed out Fidel.
Likewise, the UAM Rector highlighted that the challenge is that “research work should be returned to society". And that is the reason why they have developed the digital catalog of patents, which is an extensive database, and this annual fair to create innovation ecosystems.
During the first day of P4i, Fidel Rodríguez Batalla, the Rector and Vice-Rector of the UAM, and the general director of Research and Innovation of the Madrid Regional Government, Ana Isabel Cremades visited our stand to learn more about the work we do in technology transfer and how we transfer the results of our research to society and industry.
Cremades presented the second day of P4i the network of companies, universities, and research centers that carry out technology transfer in the Madrid Regional Government.
The director of IMDEA Materials, José Manuel Torralba, was in charge of giving the IMDEA Institutes pitch, which he described as “talent that is transformed into innovation”. He spoke about the pioneering projects we have been working on at the different centers since their creation 15 years ago, as well as highlighting their main scientific and technological advances.
At the end of the day the IMDEA Institutes' stand was visited by Diana Morant, Minister of Science and Innovation, who was able to see some of the prototypes on display, accompanied by Fidel Rodríguez Batalla and Félix Zamora.
Finally, the event was closed by the Minister of Science and Innovation, who announced the creation of a state platform for innovation and transfer with a specific section for patents and a service for the commercialization of academic patents.
Every year, the Madrid high-speed network for universities and research, REDIMadrid, holds a conference to share ideas and experiences with affiliated entities and network equipment suppliers. On this occasion, the XVII Jornadas REDIMadrid took place on October 18th at the IMDEA Software building, being the first face-to-face conference after the COVID-19 pandemic.
The Director of IMDEA Software Institute, Manuel Carro, was in charge of opening the event. He referred to the importance of network reliability for the development of the services provided by REDIMadrid and of research to ensure that networks continue to improve.
After the opening, the Director of the network and Associate Research Professor of the Institute, César Sánchez, gave a tour through the history and status of the network, the personnel in charge of carrying out the actions, the new developments and the upcoming challenges it faces.
David Rincón, Technical Coordinator, and Alicia Cardeñosa, Programmer, both from REDIMadrid, took up the gauntlet and presented the REM-eDDOS attack mitigation tool, which improves the security of the network. They also showed to the attendees a simulation of how it works in case of an attack.
The UPM ETSIinf professor Vicente Martín delved into quantum communications in his talk and explained in detail its application in some projects such as Quantum Flagship, EuroQCI, OpenQKD or MADQCI.
In the next talk, the digital classroom model of URJC was presented. David Pérez explained the process of digital transformation of university classrooms so that students can attend classes in a hybrid way.
Juan Carlos Rodríguez, from RedIRIS, spoke about the DNS Firewall service they have implemented in the national network, which adds to the classic security methods the possibility of doing it through DNS.
The UAM was represented by Pablo Collado. His talk dealt with security, access control and traffic shaping through L3 VPNs on Linux and presented a security model with WireGuard adding eBPF to achieve high scalability.
IMDEA Software Institute's researcher Srdjan Matic presented the paper "Measuring Web Cookies un Governmental Websites", in which together with Matthias Götze (TU Berlin), Costas Iordanou (Cyprus University of Technology), Georgios Smaragdakis (TU Delft), and Nikolaos Laoutaris (IMDEA Networks), after analyzing more than 5,500 websites from G20 countries, they found that up to 90% of them include cookies from third party trackers. This happens even in countries with strict user privacy laws.
The #JornadaREDIMadrid continued with a presentation by Álvaro Alonso, from the ETSIT of the UPM, who showed the web tool LICODE, a free software videoconferencing system that can be successfully implemented in multiple scenarios.
After the presentations from the academic world, the last part of the day was dedicated to talks by equipment and services suppliers. Ignacio Domínguez, from Telefónica, spoke about network telemetry, showing the improvement of this monitoring method compared to traditional methods. The last presentation was given by Manuel Abellán and Carmen Benítez, from Microsoft Spain. They showed how IT infrastructure can be improved in the academic environment through Azure services.
Blockchains are maintained by a network of participants, miner nodes, that run algorithms designed to maintain collectively a distributed machine tolerant to Byzantine attacks. From the point of view of users, blockchains provide the illusion of centralized computers that perform trustable verifiable computations, where all computations are deterministic and the results cannot be manipulated or undone.
IMDEA Software researchers Martín Ceresa and César Sánchez publish "Multi: A Formal Playground for Multi-Smart Contract" in which they implement an execution model that allows the study of smart contract interactions.
Every blockchain is equipped with a crypto-currency. Programs running on blockchains are called smart-contracts and are written in a special-purpose programming language with deterministic semantics. Each transaction begins with an invocation from an external user to a smart contract. Smart contracts have local storage and can call other contracts, and more importantly, they store, send and receive cryptocurrency.
Once installed in a blockchain, the code of the smart-contract cannot be modified. Therefore, it is very important to guarantee that contracts are correct before deployment. However, the resulting ecosystem makes it very difficult to reason about program correctness, since smart-contracts can be executed by malicious users or malicious smart-contracts can be designed to exploit other contracts that call them. Many attacks and bugs are caused by unexpected interactions between multiple contracts, the attacked contract and unknown code that performs the exploit.
Moreover, there is a very aggressive competition between different blockchains to expand their user base. Ideas are implemented fast and blockchains compete to offer and adopt new features quickly.
In this paper, the researchersw propose a formal playground that allows reasoning about multi-contract interactions and is extensible to incorporate new features, study their behaviour and ultimately prove properties before features are incorporated into the real blockchain. they implemented a model of computation that models the execution platform, abstracts the internal code of each individual contract and focuses on contract interactions. Even though the Coq implementation is still a work in progress, they show how many features, existing or proposed, can be used to reason about multi-contract interactions.
The Director of the IMDEA Software Institute, Manuel Carro, as well as Professor Pierre Ganty participated on September 30 in the scientific café organized within the framework of the European Researchers' Night at the Residencia de Estudiantes in Madrid together with other colleagues from the IMDEA Institutes. This annual event is promoted by the Vice-Presidency, Ministry of Education and Universities of the Community of Madrid, and coordinated by the Foundation for Knowledge, Madri+d since 2009, with funding from the European Commission, under the Marie Skłodowska-Curie Actions (MSCA).
After a warm welcome by Alicia Gómez-Navarro, Director General of the Residencia de Estudiantes, Ana Isabel Cremades, Director General of Research and Technological Innovation, was in charge of opening the event. She highlighted the fundamental work carried out by the IMDEA Institutes, both for developing science of excellence and for organizing events in which to disseminate scientific knowledge to society.
Manuel Carro and José Manuel Torralba, Director of IMDEA Materials, presented the activity in which researchers from IMDEA Institutes talked about how the research carried out at the centers - through lines, projects or contracts - helps to fulfill the 5 missions of the EU, whose common goal is to achieve a better and more sustainable future.
In this colloquium, very diverse topics were discussed, one of them focused on how to fight against cancer from disciplines such as Precision Nutrition or Nanoscience. It was also discussed how to help curb climate change by reducing waste production or promoting its reuse and manufacturing batteries or biodegradable prostheses with new materials. The workshop also focused on how to make the cities of the future much more intelligent through research into communication networks and software, and thus contribute to making them more livable spaces. In particular, Pierre Ganty mentioned that "thanks to high-precision agriculture, the data collected through software makes it possible to optimize the use of chemical products, making the process more efficient and less harmful".
In the scientific café, the problem of energy consumption was presented and in this sense Ganty expressed that the cryptocurrency "Bitcoin consumes as much energy as the whole of Argentina. The technology tries to solve very complicated puzzles that require a lot of energy. This is a real problem but cryptographers are changing the paradigm by moving to proof-of-stake, an example of natural evolution".
And finally, he delved into the idea of starting with small, achievable initiatives in the short term, as is the case of "the airline that is implementing a software for its airplane routes. A 'waze' for airplanes. The forecast is that they are going to cut CO2 emissions by 1% from the start, in addition to fuel savings".
Former IMDEA Software Institute PhD student Anaïs Querol, supervised by Professor Dario Fiore, defended her thesis last September at the Superior Technical School of Computer Science Ingineering from the Universidad Politécnica de Madrid (ETSIINF). In it, she presents cryptographic advances to create efficient blockchains that preserve transaction privacy and security.
As Anaïs explains in the abstract of her thesis, Internet was conceived decades ago as a protocol for the telematic interchange of information through networks of interconnected machines. But it has been suffering from structural problems for long, such as the centralization of services and the high level of trust that must be placed in the servers; leading to what are known as bottlenecks and cyber-attacks.
Blockchain was born in this scenario. A decentralized and transparent technology that arrived to improve the web as we know it.
Blockchains are lists of transaction records linked together and are secure due to the use of cryptographic methods distributed along the network nodes. Their main utility is to store information in a verifiable and immutable form; that is, a user can check the integrity of the data in them.
Modern cryptography offers tools such as zero-knowledge proofs (ZKPs), which make it possible to harmonize privacy and transparency. This means that it is possible to verify blockchain properties without leaking private information. In addition, there are other mechanisms such as SNARKs, which allow to verify it in an efficient way without losing security.
Querol's work demonstrates that by combining methods such as SNARKs and cryptographic commitments (CP): CP-SNARKs; modular blocks that respect privacy can be generated and combine with each other easily and securely with a compiler so that developers can create transparent and decentralized blockchains with all the guarantees of privacy and security, efficiently.
The IMDEA Software Institute has held the Thirteenth International Symposium on Games, Automata, Logics, and Formal Verification from September 21-23, 2022.
The aim of GandALF 2022 was to bring together researchers from academia and industry which are actively working in the fields of Games, Automata, Logics, and Formal Verification. GandALF covered an ample spectrum of themes, ranging from theory to applications, and stimulate cross-fertilization.
Pierre Ganty, Associate Research Professor at IMDEA Software, and Dario Della Monica, Assistant Professor at the University of Udine have co-chaired the event, which was attended by more than 20 researchers and followed by a total of 30 via live streaming.
There were four invited talks and four sessions (Logic, Automata, Logic II: Languages and Games, and Security and Robustness) divided in the three days:
-Wojciech Czerwiński, University of Warsaw, Poland
"Techniques for Unambiguous Systems"
-Javier Esparza, Technische Universität München, Germany
"State Complexity of Population Protocols"
-Dana Fisman, Ben-Gurion University, Israel
"Learning Languages of Infinite Words"
-Jerzy Marcinkowski, University of Wrocław, Poland
"Towards Multiset Semantics Database Theory: How I Learned to Stop Worrying and Love Linear Algebra"
More information at: https://gandalf2022.software.imdea.org/#scientific-program
Researchers Margarita Capretto, Martin Ceresa (IMDEA Software), Antonio Fernández Anta (IMDEA Networks), Antonio Russo (IMDEA Networks) and César Sánchez (IMDEA Software) present Setchain, a new data structure that improves the scalability of blockchains, allowing a greater number of transactions per block, which leads to a reduction in risk and costs for users.
Modern blockchains have the figure of smart contracts, programs that describe the functionality of transactions. With them, users can observe the details of a transaction from start to finish, generating not only greater confidence but also greater efficiency, as well as more opportunities.
The introduction of the Byzantine consensus algorithm to avoid attacks generated a limitation in the number of transactions inserted in the chain. Hence, there is a growing interest in improving the scalability of blockchains, i.e. improving the performance of the blockchain network to face of a high number of transactions. In this sense, the research team of IMDEA Software and IMDEA Networks has carried out a joint work that is reflected in the paper "Setchain: Improving Blockchain Scalability with Byzantine Distributed Sets and Barriers" and in the development of the Setchain application. The study is the result of a collaboration agreement between IMDEA Software, the Tezos Foundation and Nomadic Labs, with the aim of meeting the needs of the ecosystem and contributing to the development of the Tezos technology.
According to Margarita Capretto, pre-doctoral researcher at the IMDEA Software Institute, "right now a blockchain like Ethereum only allows 8,000 transactions per minute while VISA, for example, reaches 100,000. The difference is abysmal. That is why we have worked to create an application that allows us to achieve a breakthrough in this aspect and that can also be applied to any blockchain, not just Tezos".
“The main advantage of Setchain versus a classical blockchains is the scalability”, explains Antonio Fernández Anta, Research Professor at IMDEA Networks Institute. The result of their research shows that if barriers (a conceptual visualization of the boundary between blocks) are not needed too often (no more than once per second), "Setchain allows millions of new transactions to be added, whereas blockchains can usually only add thousands."
He adds, "Setchain allows to store transactions permanently and reliably, introducing order between transactions when it is indispensable. It can be used instead of blockchains when total order between records or transactions is not required, as order in this application is enforced when it is essential to introduce barriers between sets of records." Setchain achieves ordering of the blocks within the chain without requiring the transactions within the blocks to be ordered. The process works more efficiently and saves money for blockchain users.
Next steps
The authors of the study believe that Setchain can be used to implement a solution to so-called front-running, which is the action of observing a transaction request and maliciously injecting another one just like it before the observed ones are executed, in order to make a profit. This is achieved by paying a higher fee to a miner. Mempools are in charge of encoding the information of what is about to happen in the blockchains, so, anyone observing this data can predict the following transactions and act in their favor.
Fernández Anta warns that, although Setchain's application "are systems used by multiple entities that have to collaborate and may have conflicting interests, Setchain will provide them with a repository that allows them to share data without the risk of any of them manipulating it to their advantage".
The IMDEA Software and IMDEA Networks research team believes that their application can detect front-running and act as a mechanism to build a more efficient Mempool that encrypts transaction requests using multi-signature. Research professor Antonio Fernández Anta comments that the main conclusion they have reached is precisely that "in blockchains the total order requirements are often too restrictive, when most applications do not need them. Relaxing these requirements can lead to huge performance gains".
At just 21 years of age, the IMDEA Software Institute student David Mateos has been selected as backup of the Spanish team that will compete in the European Cyber Security Challenge (ECSC), from September 13 to 16, an initiative of the European Union Agency for Network and Information Security (ENISA) in which 27 European countries that organize national cybersecurity competitions participate.
It is the largest technical championship at the European level in cybersecurity, in which the best young talents from the different participating countries compete, selected through their different national competitions. The National Cybersecurity Institute (INCIBE) is in charge of organizing a competition every year to select the Spanish team.
From a very young age, David has always liked computers, and his father, computer scientist by profession, instilled this in him. But it was online games that sparked his passion for computer security. When he was about 15 years old, he wanted to win by cheating and for that he needed to know how it worked, its guts. Thanks to high doses of curiosity and Youtube video tutorials, Mateos, from Granada, began to "hack" games.
When he arrived at the University of Granada, he immediately joined the Hacking group (Hackiit), which not only allowed him to meet other students with similar interests and learn, but he also discovered the competitions. Playing with his classmates in competitions such as Capture the Flag (CTFs) is what has allowed him to participate in the national INCIBE competition.
David Mateos' adventure at IMDEA Software ends in a couple of weeks, he must return to Granada to finish his degree, but his time at the Institute has allowed him to get to know the world of research firsthand and it is clear to him that he would like to dedicate himself in the future to vulnerability research and exploit development (programs to exploit those vulnerabilities). As he says: "What I like most is the creative process of applying the technical knowledge you have to take advantage of a vulnerability and develop an exploit. Many times, you have to know the system better than the developers themselves to find and exploit vulnerabilities".
The Distinguished Professor at the IMDEA Software Institute and full Prof. of Computer Science at T.U. Madrid (UPM), Manuel Hermenegildo, gave a keynote at the Software Engineering and Software Development Technologies Society (SISTEDES) Conference, organized by the COGRADE group of the Universty of Santiafo de Compostela's Singula Center of Research in Intelligent Technologies, which was held this year in Santiago de Compostela from September 5 to 7.
The SISTEDES 2022 Conference includes the XXVI Software Engineering and Data Bases Conference (JISBD), the XVII Science and Engineering Services Conference (JCIS) and the XXI Programming and Languages Conference (PROLE).
In this edition, Manuel Hermenegildo, gave a keynote speech in the framework of the PROLE, on Wednesday, September 7, from 11:00 to 12:30. "Prolog turns 50, long live Prolog!" was the title of the lecture. 2022 has been declared the "Year of Prolog" not only to celebrate this anniversary but for the fact that, after all these years, Prolog and logic programming are still relevant for high-level programming and symbolic and explainable AI, with numerous implementations that continue to evolve, and new ones appearing continuously.
In this talk, Hermenegildo reviewed the evolution of Prolog over the years and the current state of the language and its implementations, followed by some thoughts on challenges and opportunities for the future. He also explained how they address some of these challenges in their Ciao Prolog system. Finally, he provided some ideas on how to teach Prolog and Logic Programming in general.
After more than three and a half years of project, Madrid Flight On Chip (MFoC) successfully culminates providing an important milestone for the implementation of advanced technological products and introduces disruptive changes in the design and verification of complex space systems. The researchers, engineers and technicians of the consortium organizations have positioned Madrid at the forefront of the "New Space" phenomenon in which technological innovation has enabled significant cost reductions leading to the provision of new products.
The Madrid Flight on Chip (MFOC) project was born in early 2019, as an action co-financed by the Madrid Regional Government and the ERDF European Union fund. Generating a technological development based on Multi-Processor System on Chip (MPSoC) components was the maxim of the project, whose main objective was the validation of this technology and its potential advantages over other classical solutions, for use in space equipment and avionics.
SENER Aerospace, coordinator of the project, led the MFOC consortium formed by the IMDEA Software Institute, Carlos III University of Madrid (UC3M), CENTUM Digital, GENERA Tecnologías and MARM.
SENER Aerospace carried out system engineering, architecture, implementation and integration tasks, as well as validation and verification of the results obtained; IMDEA Software was responsible for the preparation of a report about the state of the art and practice, and for the "MAZACOTE" tool; UC3M for the software architectures, the reliability solution, communications and the "university satellite" application; REUSE for the system engineering environment and life cycle management; and Centrum, Genera and MARM for the design and implementation of software modules and FPGAs.
The IMDEA Software Institute’s team, formed by the researchers Alessandra Gorla, José F. Morales, Fernando Macías, Daniel Jurjo and Juan F. García, has fulfilled the individual objectives set by the project, which consisted of investigating the state of the art on the technical and practical side -including both research articles and industrial tools and solutions-, as well as creating a prototype tool to generate tests automatically. Both objectives are aimed at meeting the need to substantially reduce the costs of the testing phase in the production of satellites.
In this sense, IMDEA Software has analyzed 319 articles related to automatic test generation and has concluded that the most advanced techniques and tools can be adapted to the aerospace field and that the particularities of aerospace software make it a great candidate for automatic test generation. In addition, they have created the MAZACOTE tool: "Model-Aided fuZzing And COncolic TEsting" that allows the automatic generation and execution of unit tests and reporting for model-based embedded aerospace software and whose preliminary results are encouraging. Automatic test generation does not necessarily alter internal processes towards certification but can replace or complement manual tasks.
The end of MFOC, with the consequent technology development, has represented a major advance in small satellite processing technology over existing capabilities. Furthermore, the collaboration that has been generated between the members of the Consortium during the duration of the project is intended to be sustained over time by combining and increasing the capabilities that each of these entities has separately, making Madrid an area of technological excellence in Southern Europe.
**ACTION CO-FINANCED BY THE MADRID REGIONAL GOVERMENT AND THE EUROPEAN UNION THROUGH THE EUROPEAN REGIONAL DEVELOPMENT FUND 2014-2020 (ERDF). MADRID-FLIGHT-ON-CHIP PROJECT / EXP. 49.520608.9.18 / OPERATION CODE DGII/01/21/003-18
The State Research Agency has recently published the proposed provisional resolution of selected and reserve applications for the 2021 call for Juan de la Cierva-training grants and Ramón y Cajal contract grants.
The Assistant professor at the IMDEA Software Institute, Thaleia-Dimitra Doudali, has been selected for a Juan de la Cierva-training grant, for a total value of 64,800 euros funded by the Ministry of Science and Innovation, the State Research Agency and the European Union through NextGenerationEU. The purpose of these grants is to promote the hiring by Spanish research organizations or R&D centers of young PhD graduates for a period of two years to complete their postdoctoral research training in Spanish R&D centers other than those where they completed their predoctoral training.
The Assistant professor of the IMDEA Software Institute, Marco Guarnieri, has been awarded a Ramón y Cajal grant, for a maximum value of 236,350 euros for 5 years, financed by the Ministry of Science and Innovation, the State Research Agency and the European Union through NextGenerationEU. The purpose of these grants is to promote the incorporation of Spanish or foreign research personnel, with an outstanding career, in Spanish R&D centers so that they acquire the competencies and capabilities that will allow them to obtain a stable position in a research organization of the Spanish Science, Technology and Innovation System.
**RYC-2021-032614-I and FJC2021-047102-I funded by MCIN/AEI /10.13039/501100011033 and by the European Union NextGenerationEU/PRTR.
Researchers Matthias Götze (TU Berlin), Srdjan Matic (IMDEA Software), Costas Iordanou (Cyprus University of Technology), Georgios Smaragdakis (TU Delft), and Nikolaos Laoutaris (IMDEA Networks) have presented at the 'Web Science Conference' the paper: "Measuring Web Cookies in Governmental Websites", in which they investigate governmental websites of G20 countries and evaluate to what extent visits to these sites are tracked by third parties. The results reveal that in some countries up to 90% of these websites add third-party tracker cookies without users' consent. This occurs even in countries with strict user privacy laws.
The study
Previous studies have shown the widespread use of cookies to track users on websites on an unprecedented scale but this had not been studied so far on government sites.
The researchers considered studying the behavior of government websites and their compliance or non-compliance with data protection laws during the COVID-19 pandemic, a time when citizen information was provided through official websites of international organizations and governments. "Our results indicate that official governmental, international organizations' websites and other sites that serve public health information related to COVID-19 are not held to higher standards regarding respecting user privacy than the rest of the web, which is an oxymoron given the push of many of those governments for enforcing GDPR," comments Nikolaos Laoutaris, Research Professor at IMDEA Networks.
A total of 5,500 websites of international organizations, official COVID-19 information and governments of G20 countries were analyzed: Argentina, Australia, Brazil, Canada, China, France, Germany, India, Indonesia, Italy, Japan, Mexico, Russia, Saudi Arabia, South Africa, South Korea, Turkey, UK, and the USA.
Methodology: types of cookies
There are several types of cookies. “Two primary types of cookies: first-party cookies that are issued by the visited website, and third-party ones which are typically created by external parties embedded in a webpage”, highlights Srdjan Matic, Researcher at IMDEA Software. This paper also distinguishes between cookies by their duration: session cookies active only during the visit to the page or persistent cookies of short, medium or long duration.
Results: G20 government websites
Most of the websites of the G20 countries analyzed install at least one cookie without the user's consent. Japan is the country with the lowest percentage of websites with cookies, with 77.2%, and South Korea, Saudi Arabia and Indonesia lead the ranking with almost 100%.
Figure 1. Percentage of government websites (number in parenthesis) that contain ≥ 1 cookie per G20 country.
With respect to the third-party cookies, the paper differentiates between generic third parties (TP) and third-party cookies originating from known trackers (TPT). Overall TP cookies range from 30% in the case of Germany, up to 95% for countries such as Russia. Germany is the only country where this percentage decreases significantly, with only 9% of official websites including a TPT cookie.
Figure 3. Percentage of government websites with third-party (TP) and third-party tracker (TPT) cookies per G20 country.
In 16 of the 19 analyzed countries more than half of the TP cookies last at least one day.
Figure 5. Percentage of TP and third-party trackers (TPT) cookies with expire times ≥ a day for G20 countries.
In the figure below, cookies are grouped on their expiration time into first-party (FP), third-party (TP), and third-party tracking cookies (TPT). France and China lead the ranking with around 70% of TP and TPT cookies expiring after more than one year.
Figure 7. Expiration times for first-party (FP), third-party (TP), and third-party trackers’ (TPT) cookies at G20 countries.
Results: International Organizations websites
The study shows that around 95% of the websites of international organizations set cookies and around 60% of these websites use at least one third-party (TP) cookie. Matic explains that " it seems that there is no special care in designing those webpages since 52% of websites of international organizations set at least one TPT cookie".
Results: COVID-19 Websites
More than 99% of the websites analyzed in the COVID-19 information study add at least one cookie without the user's consent. In contrast, there is a lower presence of third-party (TP) cookies, at around 62%.
As Laoutaris points out, with this publication the research team aims to "put more pressure on governments to clean up their own house first and, by doing so, set an example and be more convincing about the importance of implementing the GDPR in practice".
The IMDEA Software pre-doctoral researchers Andoni Rodríguez, Aristotelis Sibetheros, Arpit Gogia, Claudia Bartoli, Daniel Domínguez, David Balbás, Diego Castejón, Elizaveta Vasilenko, Emanuele Giunta, Gibran Gómez, Javier Galindos, Karthik Ramakrishnan, Miguel Morona, Nicolas Manini and Zilong Wang have participated in the first "My I[M]DEA Show Your Work Day", presenting posters.
The event started at 11:00, with lightning talks in which the 15 participants had up to one minute to capture the attention of the attendees and invite them to stop by their poster to explain in detail their work.
From 12:00 to 13:15 the participants were able to attend all those who were interested in their posters and tell them about their object of study. In addition, they also had the option of listening to other participants.
After the presentations, the Institute offered a lunch to all the attendees of the event and during the lunch, the judges voted (with a weight of 70%) and evaluated the popular vote (with a weight of 30%) to issue a verdict.
Nicolas Manini won first prize for his poster "Online Simulation Reduction" based on a paper also authored by Pierre Ganty and Francesco Ranzato. Javier Galindos won the second prize with the poster entitled "Toward Generalizable Cloud Resource Forecasting Using an Image-based Machine Learning Pipeline", supervised by Thaleia Doudali. And finally, Aristotelis Sympetheros with the poster "Learning Memory Access Patterns using Machine Learning and Computer Vision", also supervised by Thaleia Doudali.
The IMDEA Software Institute has been part of the list of liaison entities, universities and research centers of the "Madrid Innovation Transfer Zone" -a space from the Madrid Regional Government organized by Madri+d-, at the Digital Enterprise Show (DES), which took place from June 14 to 16, in Málaga.
Nearly 15,000 people (exhibitors, speakers and visitors) were present at the 2022 edition of DES. An event that was opened with a keynote by Barack Obama, and visited by numerous high-ranking politicians. It was inaugurated by the President of the Government, Pedro Sánchez; the President of the Junta de Andalucía, Juanma Moreno; and the Mayor of Málaga, Francisco de la Torre. And it was closed by the Minister of Tourism, Reyes Maroto.
The "Madrid Innovation Transfer Zone", was visited by several personalities: the Minister of Local Administration and Digitization, Carlos Izquierdo; the Deputy Minister of Universities, Science and Innovation, Fidel Rodríguez-Batalla; the Director General of Research and Technological Innovation, Ana Isabel Cremades; the Deputy Director General of Technological Innovation, Vicente Parras; the Director of Madri+d, Federico Morán; and the Director of Madrid Digital, Elena Liria.
Three days in which IMDEA Software and IMDEA Networks institutes shared a booth at the world's largest digital transformation event. The communication managers of both institutes, Blanca Gutiérrez (IMDEA Software) and Marta Dorado (IMDEA Networks) attended on behalf of both institutes and explained the projects and research being carried out at their centers to the visitors and other exhibitors.
The Madrid Regional Government culminates the opening of the last of the four digitization clusters in the region dedicated to Blockchain (Tres Cantos), Artificial Intelligence (Leganés), Digital Transformation (Torrejón de Ardoz) and Internet of Things (Las Rozas). Professionals from 57 leading national and international companies, organizations and entities, including the IMDEA Software Institute, comprise the clusters team with the aim of consolidating the region as a digital hub in Southern Europe, generating new business opportunities, more employment and facilitating the interaction of citizens with the public administration.
The regional government will contribute a total of 5.4 million euros - 1.8 million euros in 2022 and 3.6 million euros in 2023.
Throughout the month of May, the Madrid Regional Government, in collaboration with the City Councils of the locations of the four digitization clusters, has been holding events in which the starting signal was given by the signature of the agreement by the leading companies and institutions that will be part of these innovation spaces for the digitization clusters.
The first to start up was the blockchain cluster, located in Tres Cantos, on May 7. Its objective is to make Madrid an exporting power of this technology. The Minister of Local Administration and Digitization, Carlos Izquierdo, indicated that the agreement would "turn Madrid into the neuralgic point of connection of nodes of this technology not only with Europe but also with the American continent".
On May 9, the following presentation that took place was the Artificial Intelligence Cluster which is located in Leganés. Its main functions will be to carry out research, studies, analysis and projects in Artificial Intelligence; to promote its implementation and use; and to promote the automation of business processes.
The digital transformation cluster, located in Torrejón de Ardoz, was launched on May 18. Some of the main functions of the cluster will be: to promote the implementation, standardization and use of technologies and solutions that induce or produce digital transformation; and to respect and disseminate ethics in the development and use of digital transformation, as well as compliance with regulations regarding its research.
Finally, on May 27, the last one, the cluster dedicated to IoT (Internet of Things), was constituted with the aim of improving the quality of life of the citizens of the Madrid Regional Government thanks to the access to the new automated experiences that the IoT context offers, as well as to carry out dissemination campaigns for its understanding and to promote the implementation, standardization and use of the technologies and solutions related to IoT.
The last decade has seen a dramatic growth in cloud-based Internet services. Websites such as Amazon and Facebook process hundreds of thousands of user requests per second, yet are available at all times. To achieve this, the shared data accessed by the requests is managed by novel cloud databases that partition and replicate the data across a large number of nodes and/or a wide geographic extent.
One of the main challenges faced by cloud databases is to maintain data consistency in the presence of a massive number of concurrent modifications on different nodes, despite the inevitable failures. The classic approach is for the database to make data distribution and parallel processing transparent to the application, i.e., to behave as if it were processing serial application requests on a single, unsplit copy of the data. This strong consistency model makes it easier for the programmer to build correct applications. Unfortunately, achieving this requires the various database nodes to synchronize, which undermines the benefits of parallelism.
This has motivated academia and industry to explore alternative architectures for cloud databases that relax the synchronization between their nodes. This enables high availability and low latency by allowing one database node to respond to a request without contacting the others. It also enables high scalability, as adding more nodes to the database translates into higher throughput. Finally, the relaxation of synchronization creates more parallelism and thus uses the available hardware more cost-effectively. However, there is a downside: databases that relax synchronization expose applications to the undesirable effects of parallelism. The resulting programming models are very difficult to use correctly, and we currently lack advanced methods and tools to help programmers in this task.
The goal of the RACCOON ERC project is to develop a synergy of novel reasoning methods, static analysis tools, and database implementation techniques that maximize the effects of cloud database parallelism while enabling application programmers to guarantee correctness. To this end, we first develop methods to formally reason about how weakening the consistency guarantees provided by cloud databases affects the correctness of the application and the parallelism allowed within the databases. This is based on techniques from programming languages and software verification. The resulting theory serves as the basis for practical implementation techniques and tools that take advantage of database parallelism, but only to the extent that its side effects do not affect applications.
This afternoon took place at IMDEA Software, the Workshop "How to ride the research rollercoaster: effective presentation skills", offered by Prof. Thaleia Dimitra Doudali, in which the participation was massive.
A fundamental skill throughout the career of a researcher is to effectively present their research, a paper, a poster or a new idea to other researchers, industry, and society. Presentation skills are necessary for PhD candidates to successfully defend their dissertation and for researchers to give engaging talks and effectively pitch their research ideas during conferences, poster sessions, networking events and job interviews.
The seminar talk included advice on how to create engaging presentations, practical tips and tricks on how to structure a slide deck and a poster and practice how to best communicate research ideas. The agenda included the folowing:
At the end, group dynamics were carried out and the event was very interactive and practical.
“What’s new?” This is what users wonder when they see the notification that a mobile app has just been updated on their device. New releases may involve simple bug fixes, or may include new features that users are eager to try. Regardless of the change, users do want to know what are the differences with respect to the release that have been using so far.
IMDEA Software researchers Daniel Domínguez-Álvarez, Daniel Toniuc and Alessandra Gorla publish "ReChan: An Automated Analysis of Android App Release Notes to Report Inconsistencies", an analysis tool that allows to know if mobile app update descriptions match actual changes.
The Google Play store has a visible section for each Android app that clearly describes the changes that affect the latest release. This description, however, is curated by developers, and may not match the actual changes in the binary code. This paper presents ReChan, a novel technique aiming to automatically detect mismatches between release notes of Android applications and the actual changes in the code.
They define a taxonomy of 9 release categories by manually tagging 1,200 real samples, and present their solution to automatically classify release notes written in English. ReChan then implements specific analyses to detect such changes in the code, and compares the analyses outcome to detect mismatches.
ReChan achieves a precision, recall and f-score of 84.9% on the manually crafted ground truth of three open source apps. Experiments on a dataset of 12,706 closed source Android apps show that developers tend to correctly report changes due to bug fixes and new features, but omit changes that affect the list of requested permissions, the UI and other content that the app uses.
The IMDEA Software Institute PhD Student, Felipe Gorostiaga, successfully defended his doctoral Thesis this morning at the UPM's School of Computer Engineering (ETSIINF) at the Montegancedo Campus. Some of his colleagues were present to listen and show their support.
His Thesis, supervised by César Sánchez, is entitled: "Theory and Practice of Stream Runtime Verification for Sequences and Real-Time Event Based Systems".
Felipe started the defense stating that software verification is the employment of formal methods to ensure the absence of errors in a program, but whose application is susceptible to become impractical for large and complex systems. By contrast, runtime verification is a technique for software assurance that consists of generating, from a formal specification, a monitor that analyses an execution trace online or offline and detects violations of the specification, which makes this technique more scalable than static verification.
Stream Runtime Verification (SRV) defines specifications declaratively in terms of input and output streams of events that carry data of rich types. One of the main concerns of SRV languages is the clean separation of temporal and data aspects of a specification. In this sense, Gorostiaga commented that most early SRV formalisms, such as the pioneer language Lola, are based on synchronous streams, where data observed at the same index in different streams are considered to have occurred simultaneously.
The first contribution of this Thesis is Striver, a novel SRV language inspired in Lola that handles non-synchronized timestamped event streams. He compared Striver with similar pre-existing formalisms and also exhibit the conditions under which Striver is equally expressive to Lola.
In his work, he shows an algorithm to translate to one another and studies the performance of the translated specifications both theoretically and empirically.
The second contribution of this Thesis is the implementation of Lola and Striver using "lift-deep embedding", a novel technique that permits to effectively fulfill the promise of a straightforward addition and usage of arbitrary data types in the languages, which he demonstrates empirically employing the tools over a wide range of application domains.
Lastly, he also presented new extensions to both languages that amplify their expressive power and give rise to a new class of specifications.
The 4th edition of the "I have a project" award of the Institute of Physical and Information Technologies "Leonardo Torres Quevedo" (ITEFI) for the best final degree or master's thesis granted the first prize to David Balbas, PhD Student at the Institute IMDEA Software, at the CSIC's Serrano Street headquarters on May 12th.
Balbas' project, entitled "Secure Administrators for Group Messaging Protocols", studies group messaging from a security point of view, and in particular, asynchronous group key exchange protocols. Group instant messaging protocols, such as WhatsApp or Signal Messenger, must preserve the confidentiality and authenticity of sent messages.
David's main contribution is the formalization of the administration of a messaging group, which is the usual scenario in which there is a restricted group of users, (the administrators) with the ability to add and remove members. For this purpose, the cryptographic primitive "administrated continuous group key agreement" (A-CGKA) is introduced, along with a definition of correctness and a discussion of security models. Finally, it presents two practical modular constructions of A-CGKA using digital signatures.
In the paper, he proposes a formalism and cryptographic protocols that allow managing messaging groups with strong security guarantees. All this represents an advance in security, protecting against certain attacks, and can be applied to protocols such as those used in the world's largest instant messaging applications, which are used by billions of people every day.
Digital signatures are widely deployed to authenticate the source of incoming information, or to certify data integrity.
"Progressive And Efficient Verification For Digital Signatures", is a paper by Cecilia Boschini (Reichman University), Dario Fiore (IMDEA Software Institute), and Elena Pagnin (Lund University) that advances an innovative model for digital signature verification.
Common signature verification procedures return a decision (accept/reject) only at the very end of the execution. If interrupted prematurely, however, the verification process cannot infer any meaningful information about the validity of the given signature. We notice that this limitation is due to the algorithm design solely, and it is not inherent to signature verification.
In this work, they provide a formal framework to handle interruptions during signature verification. In addition, they propose a generic way to devise alternative verification procedures that progressively build confidence on the final decision. Their transformation builds on a simple but powerful intuition and applies to a wide range of existing schemes considered to be post-quantum secure including the NIST finalist Rainbow.
While the primary motivation of progressive verification is to mitigate unexpected interruptions, they show that verifiers can leverage it in two innovative ways. First, progressive verification can be used to intentionally adjust the soundness of the verification process. Second, progressive verifications output by our transformation can be split into a computationally intensive offline set-up (run once) and an efficient online verification that is progressive.
Quantum computing and quantum communications have the potential to become a game changer in computer networks. For this reason, IMDEA Software has undertaken together with seven other partners (IMDEA Networks, Instituto Nacional de Técnica Aeroespacial, Centro Español de Metrología, Fundación Vithas, Universidad Autónoma de Madrid, Universidad Politécnica de Madrid and Universidad Complutense de Madrid) a new project funded by the Community of Madrid, the State through the Recovery, Transformation and Resilience Plan, and the European Union through the NextGeneration EU Funds.
The objective of MadQuantum-CM is the expansion of the new quantum communications network of the Community of Madrid, interconnecting universities and research centers, as well as the development of use cases and innovations that take advantage of the deployed infrastructure.
IMDEA Software's participation in the consortium is key due to its experience in dark fiber bidding in the context of REDIMadrid and its previous participation in the European OPENQKD project.
The more than 18.5 M€ of funding will go towards providing a unique quantum communications technology development environment with the aim of becoming a permanent node of the European Quantum Communications Infrastructure (EuroQCI). MadQuantum-CM will also allow realistic demonstrations not only of the capabilities of the technologies in production environments but also of the services that can be provided by quantum networks such as critical infrastructure protection, highly secure database connections, symmetric key distribution for defense services, applications in banking, medicine, etc.
**MadQuantum-CM was supported by the MCIN with funding from the European Union NextGenerationEU (PRTR-C17.I1) and by the Community of Madrid.
Lukas Aumayr (TU Wien), Sri AravindaKrishnan Thyagarjan (Carnegie Mellon University), Giulio Malavolta (Max Planck Institute for Security and Privacy), Pedro Moreno-Sánchez (IMDEA Software Institute) and Matteo Maffei (TU Wien) have developed Sleepy Channels, a bi-directional Payment Channel protocol that keep cryptocurrencies safe without watchtowers and even if the parties are not online.
PC are a promising solution to the scalability issue of cryptocurrencies. It allows users to perform arbitrary many transactions off-chain without needing to post everything on the blockchain. However, they usually suffer from a severe limitation: both parties need to constantly monitor the blockchain to ensure that the other party did not post an outdated transaction that can potentially revert honest user’s balance. Extrapolating this issue to the banking use case, this would mean that you need to login to your bank account frequently (e.g., at least once per day) in order to ensure that your funds are there.
The figure of the watchtowers was introduced by the community as a service to mitigate this limitation (e.g., imagine a prolonged electricity cut or your phone runs out of battery for a long time). Such watchtower service charges every user a service fee and, perhaps more importantly, it is aware of sensitive financial information related to the users. Moreover, watchtowers have to lock a certain number of coins per user to be held accountable, a financial burden that have hindered the wide deployment of watchtowers in practice.
Pedro Moreno-Sánchez, and his research colleagues, have developed Sleepy Channels to solve this problem. This protocol is compatible with any blockchain that is capable of verifying digital signatures as shown by their proof of concept and no longer requires watchtower services or additional trust assumptions other than already existing ones for blockchains like Bitcoin. Thereby, this protocol enables a smooth user experience where users need to check their payment channel only for their payment operations (and of course once to close it when no longer needed).
The headquarters of the Integral Domotics Center(CEDINT) and Madrid Supercomputing and Visualization Center (CeSViMa) hosted today the official presentation of the Madrid Quantum Communications Infrastructure (MadQCI) project. The Minister of Science and Innovation, Diana Morant, and the Deputy Minister of Universities, Science and Innovation, Fidel Rodríguez Batalla attended the event, organized by the Ministry of Science and Innovation with the support of the Madrid Regional Government. Among other authorities, representatives of the beneficiary organizations were also present. The IMDEA Software Institute was represented by Manuel Carro, as director, and César Sánchez, representing REDIMadrid.
MadQuantum-CM is a project that is part of the "Complementary R&D&I Plans" of the "Recovery, Transformation and Resilience Plan" within the line dedicated to quantum communication. This is a new instrument to establish collaborations between the State and the autonomous communities in R&D&I actions. For this reason, MadQuantum-CM has joint financing through the execution of regional, state and European funds (NextGenerationEU funds, MRR).
MadQuantum-CM's main partners include the Polytechnic University of Madrid (UPM); the IMDEA Software Institute; the Spanish Metrology Center (CEM); the Complutense University of Madrid (UCM); the Autonomous University of Madrid (UAM); the National Institute for Aerospace Technology (INTA), and the IMDEA Networks Institute.
More than 18.5 M€ will be allocated to provide a unique quantum communications technology development environment with the aim of becoming a permanent node of the European Quantum Communications Infrastructure (EuroQCI). In addition, MadQuantum-CM will also allow realistic demonstrations not only of the capabilities of the technologies in production environments but also of the services that can be provided by quantum networks such as critical infrastructure protection, highly secure database connections, symmetric key distribution for defense services, applications in banking, medicine, etc.
MadQuantum-CM was supported by Ministry of Science and Innovation with funding from European Union NextGenerationEU (PRTR-C17.I1) and by the Madrid Regional Government.
The IMDEA Software Institute participated in the 'XI Madrid is Science Fair' together with the other IMDEA Institutes from March 2nd to 5th, at the IFEMA Exhibition Center. The event was organized by the Fundación para el Conocimiento Madrimasd and promoted by the Madrid Regional Government.
On Friday, March 4, the Regional Minister of Education, Universities and Science, and Presidency, Enrique Ossorio, visited the IMDEAs stands together with the Deputy Regional Minister of Universities, Science and Innovation, Fidel Rodríguez-Batalla; the Deputy Regional Minister of Educational Policy of the Regional Ministry of Education, Rocío Albert; and the General Director of Research and Technological Innovation, Ana Isabel Cremades. The delegation was received by the directors and general managers of the seven IMDEA institutes. Altogether they visited each stand to learn about the activities represented there from the researchers.
More than 20,000 people saw what educational centers, universities, companies, research centers and representatives of the Community of Madrid offered in #MadridEsCiencia.
Four intense days in which the IMDEA Institutes were able to show the young public what they are working on. Specifically, IMDEA Software presented four activities as similes of the work being done at the institute given that their work is intangible. They used the hanoi towers to show how an algorithm works and its relation to the functionality of databases; encryption disks to introduce visitors to cryptography; parallel sums to explain the divide and conquer and consensus algorithm; and finally, we explained how Instagram filters work with logic games and matrices.
The Madrid Regional Goverment celebrated the 15th anniversary of the creation of the Madrid Institutes for Advanced Studies -IMDEAs-, on February 25. Created in 2007, the seven IMDEAs develop cutting-edge science and technology with the aim of generating knowledge to transform society. Overall they have attracted more than 62 million euros thanks from nearly 2,000 R&D projects.
The Regional Minister of Education, Universities and Science -and Government Spokesman-, Enrique Ossorio, participated in the commemorative ceremony of the anniversary of these institutes that took place at the Real Casa de Correos, headquarters of the Presidency of the Madrid Regional Government. The research centers are a reference in science and innovation worldwide thanks to collaborations with companies such as: Airbus, Microsoft, Google, Boeing, Acciona, Telefónica or Abengoa.
IMDEAs gathers more than 900 researchers, 50% of whom have obtained their PhDs at international centers and around 40% come from other countries. More than 300 doctoral theses have been read at these centers and their professionals have published some 5,000 articles in international journals.
A computer program, such as Microsoft Word, requires regular updates to fix bugs. Detecting and fixing problems manually is a lot of work: time-consuming and costly. For this reason, systems are emerging that allow the checks to be done automatically, without the need for a programmer to intervene.
Computer science is a broad field with two poles: the theoretical and the practical. Refinement types aim to merge these two poles and allow conventional programming to enjoy some advantages. They provide an attractive, automated form of formal verification used to check that real-world applications are correct, such as that a web application does not leak private user information. However, currently the refinement types do not provide any mathematical proof that verifies the absence of private information leakage.
The project, led by Niki Vazou, is designing a robust and practical system of refinement types to make program development faster, more secure and error-free.
In addition, CRETE aims to make formal verification so attractive that it can be used as an aid in programming courses and to promote verified programming as the de facto way to teach programming.
The researchers Thaleia Doudali, Alessandra Gorla, Niki Vazou, Silvia Sebastián (from Institute IMDEA Software) and Clara Benac (Computer Engineering Professor at the Polytechnic University of Madrid) participated as panelists at the event organized by IMDEA Software Institute on the occasion of the International Day of Women and Girls in Science: "Discussion with female researchers: why to consider and how to navigate a career in research".
The event was hybrid, some students attended in person and most of them followed the discussion via streaming.
Thaleia Doudali, Assistant Professor at the Institute, conducted the event that began with an introduction of who the panelists are and how they got to where they are today.
They talked about how frustrating it is when you don't get a paper accepted at a major conference and warned that it happens a lot. But that it is necessary to take it philosophically, follow the advice of supervisors and continue to improve that work.
For Alessandra (Assistant Professor at the Institute), her best moment was when the head of security at Google wrote an email to her, after she had published a paper, to invite her to work with them and implement what they had been doing. That was when she really understood how linked research is to industry, how useful research really is and how it can be applied in practice.
According to Clara Benac (Professor of Computer Science, UPM), the best thing about research is the freedom to decide what you want to do and to solve challenging problems, which in some cases can save lives.
In the case of Silvia (PhD student at the Institute), her beginnings in the world of research started out of her own curiosity. She had no idea what to do and so she started talking to some faculty members at University and discovered topics they were working on that she was passionate about.
Thaleia had her role models in her own home, her older siblings. They were enthusiastic about their career in computer science and electrical engineering and played an important role in the path she chosed. Even she has worked in companies during her PhD, she ended up deciding to follow her path in research given her admiration for her supervisor as well as the freedom in choosing topics to work on.
Niki's (Assistant Professor at the Institute) PhD went really smoothly, in part, because she had such a good connection with her supervisor. She trusted him and was confident that the work they were doing was good. No matter how much her work was rejected on multiple occasions, she never fell apart.
REDIMadrid, a major network infrastructure based in the Madrid Region (Spain), managed by the IMDEA Software Institute and dependent to the Madrid Regional Government, is using GenieATM to provide automated DDoS protection for the networks of public universities in Madrid.
As one of the most technologically advanced regional research networks in Europe, REDIMadrid currently provides high-speed network services for research, educational and innovation institutions. It currently interconnects 16 independent universities and research centers in the city of Madrid, serving over 290,000 users.
Atacks in DDoS networks
A DDoS (distributed denial of service) attack is a malicious attempt to disrupt traffic on a server, service or network, overwhelming the target or its surrounding infrastructure with a flood of traffic.
DDoS attacks have been prevalent among sectors such as gaming, telecom, finance, and technology. Driven by the pandemic in 2020, schools are becoming DDoS attack targets as online learning boomed. According to Kaspersky, attacks on education networks saw dramatic increase between January and June of 2020 to as much as 350%. Low barrier to entry, vulnerability of academic networks, and increased amount of valuable and confidential data, are some of the possible reasons that attract cybercriminal activities.
The role of REDIMadrid
As the network service provider for top academic and research institutions, it is crucial for REDIMadrid to adopt the highest level of network security possible - one that is scalable and adaptive to evolving DDoS threats. They decide to turn to Genie Networks to achieve this goal through the help of Axians, their regional ICT solutions partner.
REDIMarid has a GenieATM6000 deployed in its datacenter in Madrid, monitoring network traffic flowing through research institutes, universities, and innovation centers across the city at up to 40Gbit/s upstream bandwidth. REDIMadrid integrates GenieATM’s insightful traffic analysis data with their self-developed dashboard via API. With GenieATM's detection engine, normal traffic baselines can be machine-learned adaptively for each university to identify network anomalies in real-time. When an anomaly is detected, the system automatically sends out alerts to trigger a mitigation mechanism (including REDIMadrid's self-developed mitigation tool, depending on each university's preference) to scrub the affected traffic. Network administrators can get a full glance of their traffic statistics via GenieATM's in-depth traffic reporting and deep dive into an anomaly event with the Traffic Snapshot feature.
The GenieATM solution not only ensures business continuity by minimizing downtime from DDoS attacks, but also provides REDIMadrid with comprehensive visibility over the network traffic across their datacenter and academic institutions. This means total control on network security and capacity planning for all network areas, resources, users, and applications - without compromising CapEx and performance.
Press release: https://software.imdea.org/files/2022-01-20-redimadrid-genie-en.pdf
397 early-career researchers have won a European Research Council (ERC) Starting Grants. Following the first call for proposals under the EU’s new R&I programme, Horizon Europe, €619 million will be invested in excellent projects dreamed up by scientists and scholars.
The researcher of the IMDEA Software Institute, Niki Vazou, has been awarded an ERC Starting Grant worth €1.5 million, for the project "Certified Refinement Types". It will help her to launch their own project, form a team and pursue her best ideas.
The CRETE project
Refinement types are a promising verification technology that in the last decade has spread to mainstream languages (e.g., Haskell, C, Ruby, Scala, and the ML-family) to verify sophisticated properties of real world applications, e.g., safety of cryptographic protocols, memory and resource usage, and web security.
The weakness of refinement types is that they do not meet the soundness standards set by theorem provers. A sound verification system accepts as safe only those programs that never violate their specifications. Refinement type checkers (e.g., Liquid Haskell, F*, and Stainless) approximately report five unsoundness bugs per year, as opposed to only one reported by the Coq theorem prover. This rarity of unsoundness bugs in Coq is unsurprising since Coq is designed to soundly machine check mathematical proofs. Coq's soundness design recipe though cannot be directly applied to refinement type checkers that aim to practically verify real world programs.
The goal of CRETE is to design a sound and practical refinement type system. This is an ambitious goal that entails the development of a verification system that is as practical as refinement types and constructs machine-checked mathematical proofs. The system will be implemented on refinement type systems for mainstream languages (i.e., Haskell and Rust) and will be evaluated on real-world code, such as web applications and cryptographic protocols.
“Funded by the European Union. Views and opinions expressed are however those of the author(s) only and do not necessarily reflect those of the European Union or the European Research Council. Neither the European Union nor the granting authority can be held responsible for them.” Ref.: 101039196.
The new Faculty member of the IMDEA Software Institute, Thaleia Dimitra Doudali, that has recently obtained her PhD at Georgia Institute of Technology, brings with her a new research area focused on the integration of machine learning, artificial intelligence and computer vision for building fast and more efficient software systems.
She started her research career with a purely systems background. Then, she pursued an internship at AMD Research, a hardware company interested in understanding how machine learning can help build better systems, and that was when her interest for this field started.
"Thinking about how we can use images inside software systems its a very new challenge and something I am really ready to take upon because I believe its going to change how we build systems." Doudali feels that using computer vision to solve these problems is going to be a new trend that will last at least a decade.
Going from PhD to Faculty is something rare but she feels totally prepared thanks to her Phd advisor at Georgia University, Ada Gavrilovska. She knows she has made the right decision.
In addition, Thaleia is very committed to solving the gender gap in scientific careers and wants to become a rol model, just as the ones she had, her mother and advisor. She is also very concerned about people's mental health and happiness as a driving force for life and wants to dedicate part of her time to listen, train, share and guide people.
The IMDEA Software Institute has been recognized with the ‘HR Excellence in research’ award, given by Euraxess. The European Commission recognizes with the "HR Excellence in Research Award" the institutions which make progress in aligning their human resources policies to the 40 principles of the Charter & Code, based on a customized action plan/HR strategy.
In 2020, as part of its commitment to bring the best researching talent to Madrid, the IMDEA Software Institute signed the declaration of participation in the "HR Strategy for Researchers". In 2021, after carrying out self-evaluations to identify gaps, the IMDEA Software Institute elaborated its first action plan.
Euraxess outcomed that the award reflects the commitment to continuously improve their human resource policies in line with the European Charter for Researchers and the Code of Conduct for the Recruitment of Researchers, and the commitment to achieve fair and transparent recruitment and appraisal procedures.
Pepe Vila and Joaquín Arias, two former PhD students of the IMDEA Software Institute, have won the 2019-2020 Outstanding Thesis Award granted by the Polytechnic University of Madrid (UPM).
Pepe Vila's thesis, "Learning Secrets and Models from Execution Time", directed by Dr. Boris Köpf, studies problems arising in computer systems that leak information through execution time by focusing on how such leaks can be used to learn secrets - from confidential computations - or models - from the underlying components - providing examples that violate prior assumptions about the security of systems or about the limits of an attacker. The results of his thesis evidence that better models and methods are needed to evaluate both the security of computer systems and measures against cyberattacks.
Dr. Manuel Carro, director of the Institute, supervised Joaquín Arias' thesis: "Advanced Evaluation Techniques for (Non)-Monotonic Reasoning Using Rules with Constraints". Joaquín's thesis contributes to the state of the art of both, Tabled Constraint Logic Programming (TCLP) and Contraint Answer Set Programming (CASP). His results envision advantages on several fronts: complex queries and non-trivial reasoning can be easier to express thanks to the higher-level of logic programming and constraints; fewer computations are needed thanks to the automatic reuse of previous inferences; queries and associated actions (if any) can be programmed using the same formalism. The use of the resulting tools, Mod TCLP and s(CASP), makes it easier translation of problem requirements into code and minimizes the amount of re-engineering needed to comply with the requirements when they change.
34 students from IES Camilo José Cela (Pozuelo de Alarcón) and Francisco Umbral (Ciempozuelos) took part in the "Gymkhana: Software Matters", organized by the IMDEA Software Institute on the occasion of the XXI Science and Innovation Week, organized by the Madrid Regional Government in collaboration with Madrimasd.
The director of the Institute, Manuel Carro, began talking to students and teachers about the research carried out at the institute and the profiles that are recruited. He also introduced the Director General for Research and Technological Innovation, Ana Isabel Cremades, who wanted to emphasize the commitment of the Madrid Regional Government to science and the need to awaken new vocations that can work in places like the IMDEA institutes.
Blanca Gutiérrez, Communication Manager of the Institute, presented the activity and gave the fundamental guidelines to the 14 to 16 year old students.
There were five teams that had to go through the five stations of the Gymkhana. Each of the stations addressed software-related topics such as: artificial intelligence, concurrency, parallel addition, program analysis and verification, and cryptography.
The groups followed the directions on a map, this way they knew which base station to go to at any given time. In addition, they had a limited amount of time to spend at each base station.
Once the "Gymkhana: Software Matters" was over, the groups met in the Lecture Hall, where the researchers tallied the scores until the winning team was chosen. Finally, prizes were awarded to the five members of the winning team, from IES Camilo José Cela.
The 2021 edition of the REDIMadrid Conference has been completely virtual due to COVID-19, but efforts have been joined to make the day very interesting and shorter to continue attracting a very determined audience.
Manuel Carro, Director of IMDEA Software Institute, opened the conference with a brief introduction and gave way to Ana Isabel Cremades, Director General of Research and Technological Innovation of the [Madrid Regional Government], who was in charge of the opening speech of the day together with Manuel Carro.
Manuel and Ana spoke about the origin of the network as well as the high speed networks to offer services to the educational and scientific community. In this sense, he stated that teleworking, forced by the emergence of the pandemic, would not have been possible without fiber optic networks such as REDIMadrid.
"The State of REDIMadrid. Present and Future" was the first presentation, given by César Sánchez, Director of REDIMadrid and Associate Research Professor at the IMDEA Software Institute, in which he stated that REDIMadrid is the last mile of the RedIRIS network in Madrid as part of the European GEANT network. He talked about the evolution of REDIMadrid in the coming years alluding to the new quantum network of the Madrid Regional Government, MADQCI.
David Rincón, coordinator of REDIMadrid, spoke about the Denial of Service (DDoS) attacks in the educational environment that originated the tender of a software to mitigate these attacks. The mitigation of traffic is done before it reaches the institutions, therefore, the network clients are protected. He also commented on the data of the new tool that will be put into service during 2022, REDIFoD.
The next presentation: "Hybrid recommender system for audiovisual resources", was given by José Antonio Ledesma, a computer engineer with studies focused on computing. The work he presented has been developed as a final degree project at UNED under the direction of Professor Covadonga Rodrigo and subsequently has been professionally integrated into the UNED Play solution thanks to a grant in collaboration with the INTECCA team in Ponferrada.
Then, Wifredo Aragón gave his talk "New 100Gbps network of the UPM" in which he told the audience how the UPM network got to a connection with a capacity of 100Gbps.
The day continued with the talk "The Lockdown Effect: Implications of the COVID-19 Pandemic on Internet Traffic", based on a publication authored by Juan Tapiador, Professor of Computer Science at UC3M, and Narseo Vallina-Rodríguez, Research Assistant Professor at IMDEA Networks Institute. REDIMadrid contributed to this study by providing traffic data.
Juan Quemada, from the UPM, presented the free software projects derived from the Isabel application, where projects have been developed, such as the MCU WebRTC Linckya/Licode or the Plato SAGA project.
Finally, came the block of talks of the manufacturers, in which Telefónica, Juniper Networks and Palo Alto participated. Each of them presented a paper focused on their business, Telefónica Evidence-based management and digital twin, Juniper presented its product Wifi MIST and Palo Alto talked about SASE.
Manuel Carro, director of the IMDEA Software Institute and Professor of the ETSIINF (UPM) is going to be chair together with Harald Gall, from the University of Zurich, of the "Workshop for Leaders of Informatics Research and Education" organised by Informatics Europe, that will take place the 25th of October.
The workshop will be held as part of the ECSS 2021 program and is opened to all participants. Deans and directors of Informatics universities, departments and research labs address specific challenges they encounter in their role.
The theme of the 2021 Leaders' Workshop is:
"Open Science and its Impact on Research and Career Development"
The growing relevance of Open Science and its many ramifications (open publication schemes, appearance of open research data, open source, reproducibility, public value, ...) poses a challenge, and may be a turning point, to current academic and research practices. Open Science proposals driven by researchers and academics are gathering considerable traction. At the same time, institutions at all levels (from single organizations to supra-national entities) are launching and actively supporting very ambitious plans to implement the very broad idea of Open Science, sometimes focusing on specific pillars.
The workshop is planned as a mix of talks, discussions, knowledge sharing, exchange in smaller groups, and a consolidation and presentation of the results to all participants, with ample time for interaction, discussion, and Q & A.
More information at Informatics Europe: https://www.informatics-europe.org/ecss/program/leaders-workshop.html
Researchers of the IMDEA Software Institute have given several talks and have been panelists at the 37th International Conference on Logic Programming (ICLP'21, the premier conference in the area of Logic Programming).
Distinguished Professor Manuel Hermenegildo presented, as an invited panelist, his point of view on the integration of different programming paradigms, as exemplified by the Ciao/CiaoPP system developed at IMDEA Software. The panel, entitled "No Logic is an Island: Internal and External Integration of Logic Programming Paradigms" presented experiences and posed several questions and future challenges about how different subareas/subformalisms of Logic Programming can be integrated with each other, and with other paradigms.
Recent PhD graduate Isabel Garcia-Contreras and PhD student Victor Perez-Carrasco presented a paper on their work with graduate student Miguel A. Sanchez-Ordaz and IMDEA Software's faculty members Jose F. Morales, Pedro Lopez-Garcia, and Manuel Hermenegildo, entitled "VeriFly: On-the-fly Assertion Checking via Incrementality". This work presents a tool for verifying or detecting errors interactively in software systems, early in the development cycle, without having to actually run the programs, in order to reduce production costs and increase software quality. Making use of the CiaoPP static analysis and verification framework, the VeriFly tool provides early, continuous, and precise assertion checking and other semantic feedback to programmers, presenting the results as colorings and tooltips directly on the program text within the integrated development environment (IDE). Experiments show that the modularity and incrementality of CiaoPP allow addressing a major challenge of such tools: responding interactively to program changes on the fly with very low latency times.
Post-doctoral Researcher Bishoksan Kafle presented a paper on his work with Graeme Gange, Peter Schachte, Harald Sondergaard and Peter J. Stuckey entitled "Transformation-Enabled Precondition Inference". This work presents a novel iterative method for solving the precondition inference problem, a non-trivial problem with important applications in program analysis and verification. The method automatically derives preconditions for the safety and unsafety of programs. The experimental evaluation shows that the method can infer precise preconditions (sometimes optimal) that are not possible using previous methods.
Faculty members Manuel Carro (Director), Manuel Hermenegildo, and Jose F. Morales were members of the Program Committee. The first two also chaired Sessions.
Several IMDEA Software Institute researchers are attending this week -from the 21st to the 24th- the Spanish Computer Science Congress (CEDI) held in Malaga. In this edition the Institute is sponsoring the event together with other companies such as: Avanade, CGI, Danysoft, Google, Homeria, and PwC among others.
On Wednesday, September 22nd, from 12:00-13:30, the first conference in which a member of the Institute participates will take place. It is the presentation of a paper: "Evaluation of the Implementation of an Abstract Interpretation Algorithm using Tabled CLP". Authors: Joaquín Arias (former PhD student of the Institute and Assistant Professor at Universidad Rey Juan Carlos) and Manuel Carro (director of the IMDEA Software Institute). On this occasion, Arias will be in charge of the presentation.
On Thursday 23rd, the Institute will participate on two occasions. First, with the presentation of a paper: "An application of KLEE to aerospace industrial software" from 10:00 to 10:30. Authors: Juan Francisco García, Daniel Jurjo, Fernando Macías, Jose F. Morales and Alessandra Gorla. In this case Jurjo will be the one to present the details of the paper. And, secondly, Manuel Carro, Director the IMDEA Software Institute, will be the Chair of the session "Fuzzy logic programming / Verification" starting at 12:00 and finishing at 13:30.
In addition, Juan José Moreno will participate in the assemblies and standing committee meetings of the SCIE and SISTEDES societies as founding member.
The event, hosted by the Superior Technical School of Computer Science Engineering of the University of Malaga, aims to serve as a meeting place for professionals preferably dedicated to research, development, innovation and university teaching, within the field of computer engineering.
CEDI, is structured as a multi-congress formed by a set of events, most of which correspond to Congresses, Conferences or Meetings that are being developed periodically. It practically covers all the fields in which computer science is currently involved, and within each one of them, the most innovative aspects and those with the greatest future projection are presented through communications, always from an eminently university and scientific perspective.
More information at: https://whova.com/portal/webapp/hybri1_202109/
A delegation from the Regional Government of Madrid, led by Fidel Rodríguez Batalla, Deputy Minister of Universities, Science and Innovation, accompanied by José Antonio Sánchez Serrano, Deputy Minister of Local Administration and Digitization, Ana Isabel Cremades, Director General of Research and Technological Innovation, and Alberto Retana de la Fuente, Director General of Digital Policy visited the IMDEA Networks' Institute headquarters yesterday afternoon.
The visit began with a meeting in which Albert Banchs and Manuel Carro, directors of IMDEA Networks and IMDEA Software, respectively, summarized some of the most recent advances in their lines of research, followed by a tour of some of the laboratories. In this case, the delegation was able to see first-hand the work being carried out in the laboratories for Millimeter Wave Networking (cutting-edge studies related to millimeter waves) and LiFi (an example of sustainability: battery-free energy to support, for example, the Internet of Things). They were also able to visit 5TONIC, an international reference laboratory for research on 5G networks, which brings together the innovation efforts of IMDEA Networks, entities such as the Carlos III University and leading companies, from Spain’s Telefónica to Ericsson.
At the end of the visit, Rodríguez Batalla underscored the importance of the work the research entities are undertaking: “Again, we have seen at ground level the excellence of the research being carried out in the Community, at IMDEA centers, and how it’s earning international recognition such as European research grants. The work being done here is for the benefit of society. It’s also an excellent example of technology transfer, and of collaboration between institutes, such as Networks and Software, which are carrying out incredible research”.
For his part, Manuel Carro emphasized the importance of close collaboration between public sector managers and researchers: "this visit demonstrates the extreme interest of the Madrid Regional Government in supporting science and research by seeking channels to use the advances and knowledge developed in the Region in favor of the citizen."
And Albert Banchs stressed: “Digital transformation offers many advantages, providing greater agility and dynamism to the economy and improved services to citizens, as well as being able to contribute to a larger and more competitive ICT sector.”
The researchers Musard Balliu from KTH Royal Institute of Technology and Marco Guarnieri from the IMDEA Software Institute have won a 2021 Privacy-Enhancing Technologies RFP Facebook Research award for their project “InferViz: Weighted inference and visualization of insecure code paths” worth $100,000.
The winners of the ‘2021 Privacy Enhancing Technologies request for proposals’ (whose deadline was April 12) have been recently announced. This research award opportunity attracted 159 proposals from 102 universities and ended with ten award recipients.
With this contest, Facebook’s goal is to help design and deploy new privacy-enhancing solutions that minimize the data they collect, process, and externally share across their products, and to provide better tools to control, measure, and mitigate privacy risks.
The project presented by Musard and Marco will focus on designing tools that enable programmers to automatically detect, evaluate, and visualize violations of security and privacy policies in programs. For this, the researchers will develop techniques and tool support for (1) inferring program-level dependencies from code, (2) checking security policies against these dependencies, and (3) helping developers visualize insecure flows violating the policy.
Marco, talking in relation to the award obtained, said: “We are both really happy and excited to start working on this project. We are looking forward to collaborate with Facebook’s researchers and to build on top of Facebook’s Infer program analysis tool.”
More information at Facebook’s Research Blog: https://research.fb.com/blog/2021/07/investing-in-academic-research-to-improve-our-privacy-technology-our-approach-and-recent-rfp-winners/
The researcher from the IMDEA Software Institute,, Isabel García successfully presented her thesis last Wednesday, July 21. "A scalable static analysis framework for reliable program development exploiting incrementality and modularity" is the title of the work developed by the researcher, directed by the distinguished professor and former director of the Institute, Manuel Hermenegildo. With this thesis, Isabel completes her doctoral studies in artificial intelligence at the Polytechnic University of Madrid (UPM).
Her object of study comes in response of the trend pattern, automatic source code analysis and verification is of great importance both at the level of software development and software maintenance.
Automatic static analysis tools allow inferring properties about software without executing it and without the need for human interaction. When these tools are based on formal methods, the properties are guaranteed to hold and come with a mathematical proof. The usage of these tools during the coding, testing, and maintenance phases of the software development cycle helps reduce efforts in terms of time and cost, as they contribute to the early detection of bugs, automatic optimizations, or automatic documentation. The increasing importance of the reliability of evolving software is evidenced by the current number of tools and on-line platforms for continuous integration and deployment. In this setting, when changes happen fast, analysis tools are only useful if they are precise and, at the same time, scalable enough to provide results before the next change happens.
In this thesis she studies scalable analyses in the context of abstract interpretation. Since a way to improve scalability is to perform coarser abstractions, she first inspect what effect this may have in effectively proving the absence of bugs. Second, she presents a framework for scalable static analyses which is generic, that is, independent of the data abstraction of the program. Isabel presents several algorithms for incrementally reanalyzing whole programs in a context-sensitive manner, reusing as much as possible previous analysis results. A key novel aspect of the approach is to take advantage of the modular structure of programs, typically as defined by the programmer, while keeping a fine-grained relation between the analysis result and the source program.
Additionally, she presents a mechanism for the programmer to help the analyzer in terms of precision and performance by means of assertions. She shows that these assertions together with incremental analysis are specially useful when analyzing generic code. All these algorithms have been implemented and evaluated for different abstract domains within the CiaoPP framework.
Lastly, she presents an application of the analysis framework to perform on-the-fly assertion checking, providing continuous and almost instantaneous feedback to the programmer as the code is written. Her initial experience with this integrated tool shows quite promising results, with low latency times that provide early, continuous, and precise “on-the-fly” semantic feedback to programmers during the development process. This allows detecting many types of errors including swapped variables, property incompatibilities, illegal calls to library predicates, violated numeric constraints, unintended behavior w.r.t. termination, resource usage, determinism, covering and failure, etc.
Two PhD researchers of the IMDEA Software Institute, Anaïs Querol and Silvia Sebastián, have participated at the UPM contest "Your thesis in a nutshell" which consisted in uploading a video with a short and not technical explanation of their thesis.
Both of them, Silvia and Anaïs were selected between the top ten and received a recognition and 500 euros prize for it. This recognition entailed participating in person in a special award event and presenting their thesis live. Anaïs was also selected by the jury to receive the second prize.
We are proud that researchers from the institute participate in events like these and even more proud of their achievements.
Researchers from the research unit "Security and Privacy" at TU Wien (Lukas Aumayr and his supervisor Prof. Matteo Maffei) in collaboration with the IMDEA Software Institute (Prof. Pedro Moreno-Sánchez, previously postdoc at TU Wien) and the Purdue University (Prof. Aniket Kate) have jointly developed a protocol that makes more secure and faster transactions in cryptocurrencies like Bitcoin.
Nowadays in cities like Tokyo we can subsist with cryptocurrencies like Bitcoin. Buying a coffee, going shopping, taking the bus, paying a taxi drive or even a meal are all accessible if you only got Bitcoin in your (electronic) wallet. This may seem strange for some European countries, -even though there are many cryptocurrencies in the market like ATM and coinradar (Spanish market)- but we are walking at a steady speed to that model that may or may not co-exist with our bank cards in the future.
The popularity of cryptocurrencies is increasing very fast due to the many advantages compared to, for example, Mastercard or Visa. Transactions are usually anonymous, decentralized and global (i.e., same currency is accepted worldwide).
But there is still work to do in security, privacy and efficiency. Fraud can be possible, users can discover information about other users that should be kept secret, the number of transactions is limited, and sometimes delays occur.
The researchers from the IMDEA Software Institute, TU Wien, and Purdue University, aware of these problems, have developed an improved protocol. The article, in which these ideas are based on, will be presented at the [USENIX Security Symposium 2021], one of the best IT security conferences worldwide.
The bottleneck of Bitcoin
"It has long been known that Bitcoin and other blockchain technologies have a scalability problem: There can only be a maximum of ten transactions per second," says Lukas Aumayr of the Security and Privacy research unit at TU Wien. "That's very few compared to credit card companies, for example, which perform tens of thousands of transactions per second worldwide."
An approach to solve this problem is the "Lightning Network" - an additional network of payment channels between blockchain users. For example, if two people want to process many transactions in a short period of time, they can exchange payments directly between each other in this way, without each individual transaction being published on the blockchain. Only at the beginning and at the end of this series of transactions is there an official entry in the blockchain.
As demonstrated by other works of Pedro (IMDEA Software Institute), the apparent privacy gain of the Lightning Network due to off-chain payments isn’t real. In fact, previous work of Pedro has demonstrated that payment intermediaries can learn who pays what to whom. This is an issue that needs to be solved for a system like Lightning Network to become widely used.
A second big issue is that “in addition, everyone in this chain has to contribute a certain amount of money, which is locked as collateral. Sometimes a transaction fails, and then a lot of money can remain locked for a relatively long time – the more people involved, the longer time it will take” says Pedro Moreno-Sánchez.
Mathematically ruling out vulnerabilities
“This project has advanced the state of off-chain payments both theoretically and practically. From the theory point of view, we have provided a formal model of the new payment system, proving mathematically its correctness and security against an adversary. Moreover, while current Lightning Network requires two rounds of communication across all participants in a payment, Blitz (the new protocol) reduces it to a single round of communication. This is a milestone result since Lightning Network and other approaches proposed so far where all using two rounds and it was unknown whether we could beat this barrier” in the IMDEA Software researcher’s words.
“In practice, a single round of communication implies great benefits in practicality” As Lukas said: In the first round, the money is locked, in the second round it is released - or refunded if there were problems. That could mean an extra day of delay for each user in that chain. With our protocol, the communication chain only has to be run through once”
Simulation proves practicality
However, it is not only the fundamental logical structure of the new protocol that is important, but also its practicality. Therefore, the team simulated in a payment channel network how the new technology behaves compared to the previous Lightning network. The advantages of the new protocol became particularly apparent: depending on the situation, such as the number of attacks and fraud attempts, the new protocol results in a factor of 4 to 33 fewer failed transactions than with the conventional Lightning network.
Pedro and Lukas are putting efforts on disseminating the results with the Lightning Network developers as well as other Bitcoin organizations. One of the most attractive points so far is that Blitz is totally backwards compatible with currently deployed technologies and could be immediately deployed as a more secure and faster alternative for off-chain payments.
Paper: "Blitz: Secure Multi-Hop Payments Without Two-Phase CommitsLukas Aumayr"
The researchers of the IMDEA Software Institute, César Sánchez and Felipe Gorostiaga together with Gerardo Schneider (University of Gothenburg), Sebastian Zudaire and Sebastian Uchitel (both from Universidad de Buenos Aires) have presented the paper: "Assumption Monitoring Using Runtime Verification for UAV Temporal Task Plan Executions" at IEEE International Conference on Robotics and Automation (ICRA 2021).
Temporal task planning guarantees a robot will succeed in its task as long as certain explicit and implicit assumptions about the robot’s operating environment, sensors, and capabilities hold. A robot executing a plan can silently fail to fulfill the task if the assumptions are violated at runtime. Monitoring assumption violations at runtime can flag silent failures and also provide mitigation and remediation opportunities. However, this requires means for describing assumptions combining temporal and quantitative data, automatic construction of correct monitors and ensuring a correct interplay between the planning execution and monitors.
"In this paper we propose combining temporal planning with stream runtime verification, which offers a high-level language to describe monitors together with guarantees on execution time and memory usage. We demonstrate our approach both in real and simulated flights for some typical mission scenarios."
IMDEA Software Institute researchers Marco Guarnieri and Pepe Vila together with Boris Köpf (Microsoft Research) and Jan Reineke (Saarland University) won a best paper award at the 42nd IEEE Symposium on Security and Privacy (S&P) for their paper “Hardware-Software Contracts for Secure Speculation”.
The paper develops a framework for defining hardware-software contracts that capture hardware side-channel security guarantees in a simple, mechanism-independent manner. The framework provides foundations for principled co-design of hardware and software for side-channel resistant systems. Using this framework, the authors characterize the security guarantees provided by recent hardware mechanisms for secure speculation; mapping each mechanism to a set of hardware-software contracts. Contracts are also the basis for secure programming, where different contracts impose distinct software-level requirements for end-to-end security.
The work was supported by a grant from Intel Corporation, Atracción de Talento Investigador grant 2018- T2/TIC-11732A, Juan de la Cierva-Formación grant FJC2018- 036513-I, Spanish project RTI2018-102043-B-I00 SCUM, and Madrid regional project S2018/TCS-4339 BLOQUES.
Data has emerged as the oil of the 21st century. The importance of data is no longer surprising, but its growing relevance is beginning to take on worrying overtones. Our lives are increasingly dependent on technology that seems to need our data. But where is our data? Where is it stored? Due to the ubiquity of the Internet, everything is now migrated to the cloud.
Zara, Spotify, Netflix, Twitter, practically all companies today use data on which they compute to give us a better service. For example, a music recommendation service should store what we have listened to and cross-reference that data with the data of other people with whom there is a match to try to deduce what else we might like. A financial service could do something similar with investment funds, which is arguably more sensitive information. The same could happen with health data, held by the public health provider or a private company. And all of them, moreover, often have personal information: addresses, email accounts, bank account numbers...
Almost all of these companies rely on external providers for their computing needs: storing data (i.e., delegating its storage) and using it to extract results by running programs on these providers' computers (delegating a computation).
How can we ensure that data and computations that are delegated to third parties are protected against espionage and run correctly? Data can be encrypted, but in order for it to be used by existing software, it needs to be decrypted. At that point, a malicious provider (or a provider that gets hacked) can inspect it and learn data that the company that stored it does not want to disclose and that the person to whom it refers probably does not want to disclose either. Similarly, it could change the program that executes the calculations and return incorrect results, which raises the question of how to check that such results are correct without redoing the computation?
Cryptographic techniques exist to solve both problems. Advancing on them and making them usable in practice is the main objective of the PICOCRYPT project (Cryptography for Privacy and Integrity of Computation on Untrusted Machines), proposed by Dr. Dario Fiore, a researcher at the IMDEA Software Institute of the Madrid Regional Government, which has recently been awarded a Consolidator ERC grant from the European Union (Horizon 2020 research and innovation programme) to receive funding worth 2 million euros over five years. The European Research Council is the European Union's most prestigious scientific and funding programme. With PICOCRYPT, the IMDEA Software Institute has been granted three projects by this programme (together with RACCOON and MATHADOR).
For Dr. Dario Fiore, cryptography is already a key component to keep our data secure during communication, but "the challenge of PICOCRYPT is to invent new cryptographic protocols to keep our data secure also during computation. The benefits of this paradigm are innumerable. For example, there are people and companies who refrain from using external IT resources because of the risks of this model. With the solutions we intend to design in PICOCRYPT, they could instead use these services securely and without having to fully rely on the providers of these services". It will therefore guarantee the integrity and privacy of computation made with data stored in the cloud and also make it efficient to ensure that delegation is cost-effective.
The IMDEA Software Institute is one of the seven IMDEA Institutes promoted by the Regional Government of Madrid with the aim of carrying out research and scientific development at the highest level.
“This project has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (Grant agreement No. 101001283)”
The 42nd IEEE Symposium on Security and Privacy have recently published the list of accepted papers for the conference that will take place from the 23rd to 27th of May. We are happy to announce that six papers from researchers of the IMDEA Software Institute are between them.
Since 1980, the IEEE Symposium on Security and Privacy has been the premier forum for presenting developments in computer security and electronic privacy, and for bringing together researchers and practitioners in the field. The 2021 Symposium will mark the 42nd annual meeting of this flagship conference, sponsored by the IEEE Computer Society Technical Committee on Security and Privacy in cooperation with the International Association for Cryptologic Research.
The following papers have been accepted:
A2L: Anonymous Atomic Locks for Scalability in Payment Channel Hubs
Erkan Tairi (TU Wien), Pedro Moreno-Sanchez (IMDEA Software Institute), Matteo Maffei (TU Wien).
Hardware-Software Contracts for Secure Speculation
Marco Guarnieri (IMDEA Software Institute), Boris Köpf (Microsoft Research), Jan Reineke (Saarland University), Pepe Vila (IMDEA Software Institute).
High-Assurance Cryptography in the Spectre Era
Gilles Barthe (Max Planck Institute for Security and Privacy and IMDEA Software Institute), Sunjay Cauligi (University of California San Diego), Benjamin Gregoire (INRIA Sophia Antipolis), Adrien Koutsos (Max Planck Institute for Security and Privacy), Kevin Liao (Max Planck Institute for Security and Privacy and Massachusetts Institute of Technology), Tiago Oliveira (University of Porto (FCUP) and INESC TEC), Swarn Priya (Purdue University), Tamara Rezk (INRIA Sophia Antipolis), Peter Schwabe (Max Planck Institute for Security and Privacy).
How Did That Get In My Phone? Unwanted App Distribution on Android Devices Stephan van Schaik (University of Michigan), Marina Minkin (University of Michigan), Andrew Kwong (University of Michigan), Daniel Genkin (University of Michigan), Yuval Yarom (University of Adelaide and Data61), Platon Kotzias (NortonLifelock Research Group), Juan Caballero (IMDEA Software Institute), Leyla Bilge (NortonLifelock Research Group).
SoK: Computer-Aided Cryptography
Manuel Barbosa (University of Porto and INESC TEC), Gilles Barthe (Max Planck Institute for Security and Privacy; IMDEA Software Institute), Karthik Bhargavan (INRIA Paris), Bruno Blanchet (INRIA Paris), Cas Cremers (CISPA Helmholtz Center for Information Security), Kevin Liao (Max Planck Institute for Security and Privacy; Massachusetts Institute of Technology), Bryan Parno (Carnegie Mellon University).
Bitcoin-Compatible Virtual Channels Lukas Aumayr (Technische Universität Wien), Oguzhan Ersoy (Delft University of Technology), Andreas Erwig (Technische Universität Darmstadt), Sebastian Faust (Technische Universität Darmstadt), Kristina Hostáková (ETH Zürich), Matteo Maffei (Technische Universität Wien), Pedro Moreno-Sanchez (Technische Universität Wien; IMDEA Software Institute), Siavash Riahi (Technische Universität Darmstadt).
PhD Defense
The IMDEA Software Institute researcher Maximiliano Klemen has successfully defended his PhD thesis on: "A General Framework for Static Resource Analysis and Profiling of (Parallel) Programs and an Application to Runtime Checking", supervised by Prof. Pedro López, on March 5th.
The goal of static cost analysis is to automatically estimate the resources used by program executions without running the programs with concrete data, as functions of input data sizes and possibly other (environmental) parameters. In this thesis he improves and extends state-of-the-art static cost analysis techniques by developing a novel, general and flexible framework for resource usage analysis that can be easily instantiated to infer a wide range of resources, notions of costs, and approximations, which can deal with different programming languages, platforms and execution models.
For some applications, standard resource analyses, which estimate the total resource usage of a program, do not provide the information required. For example, helping developers make resource-related design decisions requires knowing how such total resource usage is distributed over selected parts of a program. The novel, general, and flexible framework developed in Maximiliano's thesis solves this problem, by allowing setting up cost relations that can be instantiated for performing a wide range of resource usage analyses, including both static profiling and the standard notion of cost. He shows how to instantiate such framework to perform static profiling of accumulated cost (also parameterized by input data sizes). Such information identifies the parts of the program that have the greatest impact on the total program cost.
Moreover, parallel computing has become the dominant paradigm in computer architecture, and predicting resource usage on such platforms poses a difficult challenge. We address it by extending and instantiating our general framework for performing resource usage analysis of parallel (logic) programs. Besides cost functions, the analysis also infers other useful information to better exploit and assess the potential and actual parallelism of a system. He also develops a novel application of his cost analysis framework: inferring static performance guarantees for programs with run-time checks. Instrumenting programs for performing run-time checking of properties, such as regular shapes, is a common and useful technique that helps programmers detect incorrect program behaviors. However, such run-time checks inevitably introduce run-time overhead (in execution time, memory, energy, etc.). He proposes a method that uses static analysis to estimate such overhead. This approach can provide guarantees for all possible execution traces, and allows assessing how the overhead grows as the size of the input, which is a parameter of the estimated cost functions, grows. His method also extends an existing assertion verification framework to express “admissible” overheads, and statically and automatically checks whetherthe instrumented program conforms with such specifications.
The accuracy and applicability of his framework strongly depend on the capabilities of the component in charge of solving (or safely approximating) the cost and size recurrence relations generated during the analysis. In this thesis he proposes techniques for solving recurrence relations that extend state-of-the-art solvers, addressing some of their limitations. In particular, he develops a novel approach for solving arbitrary, constrained recurrence relations. It is a guess and check approach that uses well-known machine learning techniques for the guess stage, and a combination of an SMT-solver and a Computer Algebra System for the check stage. Additionally, he develops a method for solving cost relations involving a maximization operator, which appears when representing complex size and cost relations.
Finally, he reports on the implementation of the techniques developed in this thesis within the CiaoPP system and their experimental evaluation, obtaining encouraging results.
The researcher of the IMDEA Software Institute, Jose F. Morales, has been elected to the Executive Board of the Association for Logic Programming - ALP.
The Association for Logic Programming (ALP) was founded in 1986, with the mission to contribute to the development of Logic Programming, relating it to other areas, and to promote its uses in academia and industry worldwide.
The ALP Board is the governing body of the association and is in charge of defining priorities, supervising the journal (TPLP), organizing conferences and Summer schools, etc., and in particular proposing General and Program Committee Chairs for the different conferences organized by the Association.
ALP Executive Board members are elected by a popular vote within the community among candidates proposed for their contributions and recognition within logic programming.
PhD defense
The researcher from thr Institute IMDEA Software, Alejandro Aguirre, advised by Prof. Gilles Barthe, has recently defended his thesis successfully: "Relational logics for higher-order effectful programs".
Relational logics are used to express what properties of two executions of the same program or two executions of two different programs have in common. Properties such as program equivalence, non-interference, differential privacy, robustness or sensitivity fall under this umbrella.
Although traditional program verification offers the capability to prove relational properties by using program transformation, ultimately these fall short because they are unable to use the program structure to guide the reasoning. On the other hand, novel logics explicitly designed for relational reasoning are often overly reliant on reasoning synchronously, that is, about programs with similar syntactic structure.
In this study, Alejandro starts by developing Relational Higher-Order Logic (RHOL), a logic to prove relational properties of a pair of pure functional programs that can reason synchronously when the programs have the same syntax, but also has a wide variety of one-sided rules that allows the reasoning to progress when the programs lack this similarity. RHOL also has a companion system, Unary Higher-Order Logic (UHOL) that can be used to prove unary properties (i.e., properties of a single program). Both RHOL and UHOL are based on a standard Higher-Order Logic (HOL). RHOL is not only a logic in its own right, but can also be seen as a framework in which to embed other relational reasoning systems to prove their soundness, as well as a base on top of which to build more expressive logics.
The author demonstrates the versatility of RHOL by using it to support different extensions with the aim of reasoning about probabilistic programs. He first focus on lifting-based properties. Liftings provide a way to erase the computational side effects from logical specifications, so that they can reason about them using standard logics. Some properties that can be proven in this manner are bounds on the probability that the program output satisfies a certain property, or differential privacy. He respectively embed reasoning about these two properties into two novel logics: Higher-Order Union Bound Logic (HO-UBL) and Higher-Order Relational Probabilistic Logic (HO-RPL). He then extends these logics to support reasoning about adversarial properties that specify the behavior of a known program (an oracle) with respect to an unknown program or environment (the adversary). These properties are important concepts in fields such as security or privacy.
Also, in this study, Aguirre considers other related topics. First he looks into proving properties of Markov chains. Many of these properties are inherently relational (e.g., stochastic dominance, recurrence, transience). He adapts the Guarded Lambda Calculus, and the Guarded HOL -a language and logic to reason about infinite streams-, to his setting by extending them with probabilities and developing a relational logic on top of Guarded HOL. Second, he presents a relational logic for higher-order probabilistic programs that is not lifting-based. This requires an extension of the assertion language and an axiomatization of probability theory in the base logic. Finally, Alejandro develops a predicate transformer to reason about expected sensitivity of probabilistic programs.
With this work, the researcher Alejandro Aguirre manages to make a leap in the world of privacy and computer security. He has made several achievements that allow us to learn more about the operation of some programs with probabilistic behaviour.
Institutional visit
The Secretary of State for Digitisation and Artificial Intelligence, Carme Artigas, the Regional Minister for Science, Universities and Innovation (CM), Eduardo Sicilia, and the Director General for Research and Technological Innovation, María Luisa Castaño have visited the IMDEA Software Institute.
The director of the Institute, Manuel Carro, the deputy director, Juan Caballero, and the former director, Manuel Hermenegildo, received the personalities and took them on a tour of the facilities in which they were not only shown the building but also the cutting-edge research work.
The researcher Aleks Nanevski opened the welcome session in which he briefly explained the history of the Institute and the importance of software research. The committe was directed to the third floor where Manuel Hermenegildo spoke about green computing, and Dario Fiore and Ignacio Cascudo about cryptography, a very important part of the Institute. Juan Caballero spoke to them about computer security and the research being done at the Institute.
The visit continued with a walk through the floor to the Happening area where Alessandra Gorla briefed them on computerised testing as well as the projects she is involved in, and finally, Alexey Gotsman gave them a glimpse about distributed systems.
After the sessions with some of the institute's researchers, the visit continued to a meeting room where a private meeting was held to discuss important topics and strategies for attracting and retaining talent as well as technology transfer to the Industry.
The Secretary of State of Digitization and #AI, @carmeartigas (@SEDIAgob), @edsicilia and @CastanoMluisa, from the Council of Science, Universities and Innovation (@ComunidadMadrid) have visited us today. @IMDEAInstitutes pic.twitter.com/8utrgx8XeT
— IMDEA Software Institute (@IMDEA_Software) March 2, 2021
The researcher of the IMDEA Software Institute, Niki Vazou, has been elected as part of the members of the board of the Haskell Foundation. It is the first time the Foundation decides to create a Board of Directors, so the presence of Vazou is historic.
The Haskell Foundation Board of Directors are responsible for managing and setting the direction of the Haskell Foundation. HF's current board will serve on an interim basis during the launch phase and will manage the establishment of the first full board in early 2021.
Haskell is not “just another programming language”: it embodies a radical and elegant attack on the entire enterprise of writing software. It profoundly influences the world of software for the better. The Haskell Foundation (HF) is an independent, non-profit organization dedicated to broadening the adoption of Haskell, by supporting its ecosystem of tools, libraries, education, and research.
It is not a secret that Niki's research interests include refinement types, automated program verification, and type systems and her goal is to make theorem proving a useful part of mainstream programming. Liquid Haskell is an SMT-based, refinement type checker for Haskell programs that has been used for various applications ranging from fully automatic light verification of Haskell code, e.g., bound checking, to sophisticated theorem proving, e.g., non-interference.
Manuel Hermenegildo, Distinguished Professor at the IMDEA Software Institute, has been appointed for a second term as Chairman of the Scientific Board of INRIA, the French National Institute for Research in Computer Science and Automation (Institut national de recherche en informatique et en automatique). He will carry out that role for a new period of three years.
INRIA is a French national public research institution focused on computer science and applied mathematics. It comprises 8 research centers (in Bordeaux, Grenoble-Inovallée, Lille, Nancy, Paris-Rocquencourt, Rennes, Saclay, and Sophia Antipolis) and employs more than 3800 people, including 1300 researchers, 1000 Ph.D. students, and 500 postdocs.
The INRIA Scientific Board provides guidance on the major aspects of INRIA's scientific policy, including the development of the research centers and teams, and the appointment and renewal of directors, in agreement with the Board of Directors.
Scientific results
The researchers Dario Fiore (IMDEA Software Institute), Aikaterini Mitrokotsa (Chalmers University of Technology), Luca Nizzardo (Protocol Labs Research) and Elena Pagnin (Lund University) receive the 2020 Premium Award for Best Paper in the IET (The Institution of Engineering and Technology) for the paper: "Multi-Key Homomorphic Authenticators."
The technological innovations offered by modern IT systems are changing the way digital data is collected, stored, processed, and consumed. As an example, think of an application where data is collected by some organisations (e.g. hospitals), stored and processed on remote servers (e.g. the Cloud) and finally consumed by other users (e.g. medical researchers) on other devices. On the one hand, this computing paradigm is very attractive, particularly as data can be shared and exchanged by multiple users. On the other hand, it is evident that in such scenarios, one may be concerned about security: while the users that collect and consume the data may trust each other (up to some extent), trusting the Cloud can be problematic for various reasons. More specifically, two main security concerns to be addressed are those about the privacy and authenticity of the data stored and processed in untrusted environments.
While it is widely known that privacy can be solved in such a setting using, e.g. homomorphic encryption, in this work, the authors focus on the orthogonal problem of providing authenticity of data during computation. Towards this goal, their contribution is on advancing the study of homomorphic authenticators (HAs), a cryptographic primitive that has been the subject of recent work.
Homomorphic authenticators (HAs) enable a client to authenticate a large collection of data elements and outsource them, along with the corresponding authenticators, to an untrusted server. At any later point, the server can generate a short authenticator vouching for the correctness of the output y of a function f computed on the outsourced data. The notion of HAs studied in prior work, however, only supports executions of computations over data authenticated by a single user.
In this paper, the authors introduce and formally define multi‐key HAs, they propose a construction of a multi‐key homomorphic signature based on standard lattices and supporting the evaluation of circuits of bounded polynomial depth, and they provide a construction of multi‐key homomorphic MACs based only on pseudorandom functions and supporting the evaluation of low‐degree arithmetic circuits.
In conclusion, this paper provides an innovative solution through the notion of multi‐key HAs. This primitive guarantees that the corruption of one user affects the data of that user only, but does not endanger the authenticity of computations among the other (un‐corrupted) users of the system. Moreover, the proposed system is dynamic, in the sense that compromised users can be assigned new keys and be easily reintegrated.
This paper is an extended version (with additional results and detailed proofs) of the paper "Multi-Key Homomorphic Authenticators" presented by the same authors at ASIACRYPT 2016.
The researchers Álvaro Feal (IMDEA Networks Institute), Paolo Calciati (IMDEA Software Institute), Narseo Vallina-Rodríguez (IMDEA Networks Institute), Carmela Troncoso (Spring Lab EPFL), and Alessandra Gorla (IMDEA Software Institute) have won the "Emilio Aced Award for the Research and Personal Data Protection" given by the Spanish data protection agency (AEPD), for the paper "Angel or Devil? A Privacy Study of Mobile Parental Control Apps."
Parental control apps are used by parents to monitor the use that their children make of their mobile phones, and to block access to certain features. These apps are highly intrusive by definition, as they can track the actions and movements of the children’s phone (and thus of the child). Therefore, the use of parental control apps can have implications on the privacy of both children and parents.
The study
Existing recommendations by official bodies (such as SIP4 by the European Commission) do not take privacy into consideration, benchmarking only features such as price, capabilities, or usability. To assess such privacy risks, Álvaro, Paolo, Narseo, Carmela and Alessandra relied on a combination of static and dynamic analysis to study 46 parental control apps.
In their work, the researchers found that almost 75% of the apps contain data-driven third-party libraries for secondary purposes (namely advertisement, social networks, and analytic services) and that 67% of the apps share private data without user consent, including apps recommended by public bodies, such as IS4K (Internet Segura For Kids by INCIBE).
They also found that these apps were not transparent about their data collection practices, as 80% of the apps that share data with third parties do not name them in their privacy policy.
Conclusions
The researchers have presented the first multi-dimensional study of the parental control apps ecosystem from a privacy perspective. With their findings they open a debate about the privacy risks introduced by these apps. Does the potential of parental control apps for protecting children justify the risks regarding the collection and processing of their data? This is worrisome, as current legislation (such as the GDPR) protects children’s data from being accessed without clear parental consent. So, given the potential risks of this type of software, they recommend parents to rely on non-technical solutions when possible and to have privacy in mind when choosing one of these applications.
They believe that public bodies should take privacy into account when recommending a given parental control app to raise awareness and encourage developers to follow privacy-by-design principles. The researchers from the IMDEA Software Institute, IMDEA Networks Institute and Spring Lab EPFL stress that it is fundamental to complement current benchmarking initiatives with a security and privacy analysis to help parents to choose the best application while taking these aspects into consideration.
Joint press release Paper link
The former researcher of the IMDEA Software Institute, Platon Kotzias, defended his thesis: “A Systematic Empirical Analysis of Unwanted Software Abuse, Prevalence, Distribution, and Economics” in 2019, directed by the Associate Professor, Juan Caballero. Today he works at NortonLifeLock on a wide range of system security topics including malware detection on Android and Windows, application of AI on security topics, and network security.
This month the UPM has resolved the two winners of the Extraordinary Award and Platon's thesis is one of them. In which he investigates how Potentially Unwanted Programs (PUP) can pose significant risks to users’ security and privacy. In particular, he analyzed in both breadth and depth the PUP abuse, prevalence, distribution, and economics.
His PhD shed light on various unknown facets of PUP that affected millions of Internet users. His work has been published in top-tier security conferences like Usenix Security, ACM CCS, IEEE Security & Privacy, and NDSS Symposium.
The four contributions of the thesis
Platon Kotzias performs a systematic study on the abuse of Windows Authenticode code signing by PUP and malware. Building an infrastructure that classifies potentially malicious samples as PUP or malware and using this infrastructure to evaluate 356K samples. He also evaluates the efficacy of Certification Authority (CA) defenses such as identity checks and revocation. CA revocations were equally low for both malware and PUP, so, he concludes that current CA defenses are largely ineffective for PUP.
He measured the prevalence of unwanted software on real consumer hosts using telemetry from 3.9 million hosts. He found PUP installed in 54% of the hosts in their dataset. They also analyzed the commercial pay-per-install (PPI) service ecosystem showing that commercial PPI services play a major role in the distribution of PUP.
In his thesis, Platon performed an analysis of enterprise security and measured the prevalence of both malware and PUP on real enterprise hosts. He used AV telemetry collected from 28K enterprises and 67 industry sectors with over 82M client hosts. Almost all enterprises, despite their different security postures, encounter some malware or PUP in a three year period.
And lastly, he performed an analysis of PUP economics. He proposed a novel technique for performing PUP attribution. Then, he used it to identify the entities behind three large Spanish-based PUP operations and measure the profitability of the companies they operate. The analysis showed that in each operation a small number of people manages a large number of companies, and that the majority of them are shell companies. In the period 2013–2015, the three operations have a total revenue of 202.5M euros and net income of 23M euros. Finally, he observed a sharp decrease on both revenue and income for all three operations starting mid-2014. So, he concludes that improved PUP defenses deployed by various software and security vendors significantly had an impact on the PPI market.
Research Results
The European Research Council (ERC) announced today the awardees of its latest Consolidator Grant call for mid-career researchers. Its funding is part of the EU's current research and innovation programme, Horizon 2020, and worth in total €655 million.
The ERC has granted 327 Consolidator Grants in 2020 to researchers from 23 countries, of which 22 were given to Spanish proposals (consult statistics). The proposal of the IMDEA Software Institute researcher, Dario Fiore, with the project "Cryptography for Privacy and Integrity of Computation on Untrusted Machines (PICOCRYPT)" is one of them.
Dr. Fiore's proposal, planned for five years, has a budget of €2 million, which will allow him to consolidate his research team and make far-reaching advances. PICOCRYPT becomes the third ERC grant awarded to researchers from the IMDEA Software Institute.
The PICOCRYPT project
Due to phenomena like the ubiquity of the Internet and cloud computing, it is increasingly common to store and process data on third-party machines. In spite of its attractive aspects, this trend raises a number of security concerns, including: How to ensure that the results computed by third parties are correct (integrity) and no unauthorized information is leaked (privacy)? The current way to deal with these problems is to trust third parties under legislation guarantees. This approach assumes that third-party machines stay honest all time, even if they get hacked! This is unrealistic and contradicted by the numerous security incidents that are regularly reported.
Instead, Dr. Fiore's view is that it should be possible to store and process data on untrusted machines without risking for privacy and integrity and without the need of trusting these machines. Recent trends in cryptography promise solutions to realize this vision but the existing generation of protocols is limited due to its high costs and its poor support to emerging applications such as data stream processing. The grand challenge of this project is to invent a new generation of cryptographic protocols for commputing securely on untrusted machines in a way that is cost-effective and suitable for future application scenarios.
The solutions provided by the PICOCRYPT project will have the potential to generate a paradigm shift in the way privacy and integrity are ensured and will have an impact on the world of information technology by making delegated computing more secure not only for citizens but also for public and private organizations that, due to current risks, may give up using these services.
Research Results
The researchers František Farka, Aleksandar Nanevski, Anindya Banerjee (from the IMDEA Software Institute), Germán Andrés Delbianco (Nomadic Labs), and Ignacio Fábregas (Universidad Complutense de Madrid) have recently published "On Algebraic Abstractions for Concurrent Separation Logics", that has been accepted at POPL 2021.
Concurrent separation logic is a logic for verification of stateful programs. This logic is distinguished by transfer of state ownership upon parallel composition of threads. The semantics ownership transfer is given by the algebraic structure of partial commutative monoids(PCMs). Extant research considers ownership transfer primarily from the logical perspective while comparatively less attention is drawn to the symbolic manipulation on the level of specifications expressed in the assertion language.
This paper provides an algebraic formalization of assertion language for ownership transfer in concurrent separation logic by means of structure-preserving partial functions (i.e., morphisms) between PCMs, and an associated notion of separating relations.That is, when verifying software, they can assert specifications in symbolic languages of standard mathematics; the only concession they are forced to is relaxation from total domains to partial ones.
Morphisms, that is structures preserving maps, are a standard concept in algebra and category theory. However, morphisms haven't seen ubiquitous use in separation logic before. Separating relations are binary relations that generalize disjointness and characterize the inputs on which morphisms preserve structure. The two abstractions facilitate verification by enabling concise ways of writing specs, by providing abstract views of threads' states that are preserved under ownership transfer, and by enabling user-level construction of new PCMs out of existing ones.
The presented work constitutes a novel approach to assertion language of separation logics as the algebra of PCMs, their morphisms and constructions has not been considered before in this context.
Research Results
IMDEA Software Institute researcher, Manuel Hermenegildo, gives the Opening Invited Talk at the 27th Static Analysis Symposium (SAS'20), on "Cost Analysis of Smart Contracts via Parametric Resource Analysis," work co-authored with Víctor Pérez, Maximiliano Klemen, Pedro López-García and José Francisco Morales.
This line of research is motivated by the fact that, in blockchains, contract execution and storage are replicated across large numbers of nodes, and this makes resource consumption an important concern. The few cost analyzers that exist for smart contracts are for specific platforms and languages. However, blockchain platforms present significant variability, also over time.
Parametric Resource Analysis (also referred to as User-Defined Resource Analysis) is a generic approach, proposed by the IMDEA Software Institute team, for developing analyzers that infer safe bounds on different resources and with different resource models. In the talk, Manuel Hermenegildo reviews this approach and explores its application to the static inference of gas and storage consumption bounds for smart contracts, reporting on a concrete case study: developing an analyzer for the Tezos platform and its Michelson language. The results show that the approach is an effective method for the rapid development and maintenance of cost analyzers for smart contracts.
The Parametric Resource Analysis approach was awarded the 10 year Test-of-Time Award at the 2017 International Conference on Logic Programming, the premier conference in the area.
IMDEA Software's CiaoPP framework implements this approach and allows its application to different programming languages, by translation into a Horn clause-based intermediate representation.
The series of International Static Analysis Symposia (SAS) serves as the primary venue for presentation of theoretical, practical, and application advances in this area. This edition of SAS is co-located with SPLASH'20 in an online form, coordinated from Chicago, USA, from November 18 to November 20, 2020. SPLASH embraces all aspects of software construction and delivery, to make it the premier conference on the applications of programming languages - at the intersection of programming languages and software engineering.
The associated work is conducted in the context of the collaboration of the Tezos foundation and Nomadic labs with the IMDEA Software Institute.
The 2020 edition of the REDIMadrid Conference has been completely virtual due to the COVID-19, but efforts have been made to make the conference very interesting, shorter in order to continue to attract a very determined audience.
Blanca Gutiérrez, Communication Manager of the IMDEA Software Institute, began the conference with a brief introduction and was followed by Manuel Carro, Director of the IMDEA Software Institute, who gave the conference's opening speech.
Manuel, spoke about the origin of the network as well as high-speed networks that offer services to the educational and scientific community. In this sense, he stated that teleworking, forced by the arise of the pandemic, would not have been possible without fibre optic networks such as REDIMadrid. "The leap into the digital world and into education has come to stay despite the fact that regulations must also be updated" he confirmed.
"The state of REDIMadrid. Present and Future" was the first presentation, given by César Sánchez, director of REDIMadrid and Associate Research Professor at the IMDEA Software Institute, in which he commented that REDIMadrid is the last mile of the RedIRIS network in Madrid as part of the European GEANT network.
David Rincón, Coordinator of REDIMadrid, spoke about the Denial of Service (DDoS) attacks in the educational environment that have resulted with the tendering of a software to mitigate these attacks. "This is a new service offered by REDIMadrid which has had to be adjusted to the change in profile caused by COVID-19" he said of the GENIE tool. The traffic is mitigated before it reaches the institutions, so the network's clients are protected.
The following talk: "The Madrid Quantum Network", was given by Vicente Martín, professor of the Computer Science Faculty, UPM. His presentation was based on the quantum network that is being deployed in Madrid as part of the OpenQKD project. "Quantum computing is characterised by the basic information unit Qubit. Qubits communication consists of the propagation of photons and, when these are in transit, they cannot be touched without modifying their characteristics, for this reason they cannot be intercepted in transit and this is what gives the technology total security" confirms Vicente.
After the talk on quantum communications came the WhiteBox colloquium in which the following took part: Diego Nuevo, Network & Data Center Arquitect at Axians; Víctor López, technology expert in the General Directorate of Systems and Networks at Telefónica; and Óscar Rebollo, engineer at REDIMadrid. The situation of integration, costs and support of the whiteboxes was discussed, as well as the state of penetration of this equipment in the clients' networks, exemplified by the TIP project (Telecom Infra Project).
The conference continued with the talk "The Lockdown Effect: Implications of the COVID-19 Pandemic on Internet Traffic", based on a publication that will be presented soon and whose authors are Juan Tapiador, professor of computer science at UC3M, and Narseo Vallina-Rodríguez, Research Assistant Professor at the IMDEA Networks Institute. REDIMadrid has contributed to this study by providing traffic data.
The next to participate was Marta Vázquez, from INTECCA-UNED, who presented the AVIP application. "From COVID-19, videoconferencing has become compulsory at the UNED and thanks to the application's scalable architecture, it has been possible to absorb the large increase in traffic, which has peaked at over one hundred thousand users on some days".
And finally, Gibran Gómez, researcher at the IMDEA Software Institute, gave a talk on "Malicious TLS Traffic Detection using Unsupervised Machine Learning". According to Gibran "there are few protocols that send clear information, so attacks on protocols that use encryption such as TLS are beginning to increase. Machine Learning (ML) techniques are used to detect and combat MITM and malware attacks and the system developed detects them and generates alerts".
Research Results
The researcher of the IMDEA Software Institute, Elena Gutiérrez, supervised by Pierre Ganty, defended recently her thesis titled: "New Perspectives on Classical Automata Constructions".
She focuses in this thesis on the models of finite-state automata, pushdown automata and context-free grammars. These models have been proved useful for a wide number of applications such as program verification, natural language processing tasks or digital-image compression techniques. These applications strongly rely on language-theoretical notions where, still today, many questions are open.
The goal of this thesis is to give new theoretical perspective on a collection of open problems, that are at the core of classical automata constructions and well-established algorithms.
The underlying mathematical tool to approach these questions are equivalence relations on words as abstractions of languages. So, she studies three main questions:
In this thesis, she aims to get a better understanding of the language-theoretical basis of the double-reversal method and its connection with the partition-based techniques. As a result, we provide a uniform framework of deterministic automata constructions based on finite-index equivalences on words that allows us to give a new simple proof of the double-reversal method and shed light on the relation between this algorithm and the partition-based techniques.
Her main contribution is to provide an infinite family of PDAs defined over a singleton alphabet that allows her to extract lower bounds on the number of grammar variables of the smallest CFG.
To sum up, "in this dissertation we leverage equivalences on words as abstractions of languages. More pointedly, these abstractions are regular approximations of languages. Our results regarding finite-index congruences encourages the study of other kinds of regular approximations of context-free languages and the use of our framework to define congruence-based automata constructions for their finite representation", appointed Elena. On the other hand, her work on the Parikh equivalence assumption shows that, despite being a relaxed version of language equivalence that enables the analysis of certain complex systems, when comparing PDAs against CFGs the situation is not different to that of language equivalence. And also, sets the basis for future directions on the extension of Parikh's Theorem to weighted automata.
Research Results
The researchers Zsolt István (IMDEA Software Institute), Kaan Kara, (Oracle Labs), and David Sidler (Microsoft Corporation) have published the book "FPGA-Accelerated Analytics: From Single Nodes to Clusters".
Today datacenters that host data-intensive applications used in online services and machine learning need to store and process data that increases at an exponential rate. Data processing and management applications have become increasingly distributed and this has lead to new data movement bottlenecks at various levels of software and hardware architecture.
The authors survey recent research on using reconfigurable hardware accelerators, namely, Field Programmable Gate Arrays (FPGAs), to accelerate analytical processing. Such accelerators are being adopted as a way of overcoming the recent stagnation in CPU performance because they can implement algorithms differently from traditional CPUs, breaking traditional trade-offs.
Zsolt, Kaan and David discuss the benefits of using FPGAs in the context of analytical processing, both as an accelerator within a single node database and as part of distributed data analytics pipelines. They also present guidelines for accelerator design in both scenarios, as well as, examples of integration within full-fledged Relational Databases.
Finally, they highlight future research challenges in programmability and integration, and cover architectural trends that are propelling the rapid adoption of accelerators in datacenters and the cloud.
Research Results
The researchers Alfredo Di Napoli, Andres Löh (both from Well-Typed LLP), Ranjit Jhala (University of California at San Diego) and Niki Vazou, from the IMDEA Software Institute have presented: “Liquid Haskell as a GHC Plugin” at the Haskell Implementors’ Workshop (HIW 2020) in ICFP 2020.
Liquid Haskell is a system that extends GHC with refinement types. Constraints arising from the refinement types are sent to an external automatic theorem prover such as z3. By employing such additional checks, one can express more interesting properties about Haskell programs statically.
Up until now, Liquid Haskell has been a separate executable that uses the GHC API, but would run on Haskell files individually and just say “SAFE” or “UNSAFE”. If “SAFE”, one could then proceed to compile a program normally.
Recently, the researchers have rewritten Liquid Haskell to now be a GHC plugin. The main advantages of this approach are:
When checking source files, Liquid Haskell requires information about the constraints already established for dependent libraries. Previously, these had to be hand-distributed for selected modules with Liquid Haskell itself. Now, they become part of normal GHC interface files and can be distributed for arbitrary user packages via Hackage.
In this work, the researchers present the Liquid Haskell plugin workflow and why they think it is superior to the old approach. They also discuss the implementation of the plugin: it is interesting because it does not neatly fit into the plugin categories currently provided. Morally, Liquid Haskell typechecks the code, but in order to generate constraints to feed to the prover, it must access (unoptimised!) core code. They explain the final design, and some of the iterations they needed to get there.
For more details, check out the relevant blogs on (liquidhaskell)1 and (well-typed)2 and join (Liquid Haskell's slack)3 for feedback and questions!
Research Results
The researchers Pierre Ganty, Elena Gutiérrez and Pedro Valero have recently published "A Quasiorder-based Perspective in Residual Automata" presented at MFCS 2020 (Mathematical Foundations of Computer Science) that took place from the 24th-28th of August. The three researchers of the IMDEA Software Institute propose a different view on a class of finite-state machines of great relevance in practice, the so-called "Residual Automata".
To give a little bit of context, residual automata are classical finite-state automata (FSAs for short), i.e., transition systems with a finite number of states that are used to represent the so-called regular languages, one of the most studied objects in formal language theory.
Actually, finite-state automata are finite representations of regular languages, and this might not be illuminating but it is rather helpful when the languages they represent are infinite!
Going back to our objects, residual automata, among the general FSAs, enjoy interesting properties that make them useful in applications such as grammar inference.
The main goal of grammar inference is to find a target language using a finite set of examples of words in the language. In other words, grammar inference is a machine learning technique by means of which we learn a (possibly infinite) language of words given only a finite number of them.
In this context, residual automata are useful tools as it has been proven that they can represent very concisely (and finitely, since they are FSAs) the target language.
In this paper, they study the properties of residual automata from a theoretical point of view.
Namely, we use quasiorders as a mathematical tool to give a new perspective on the construction of residual automata. Quasiorders are relations between the elements of a set satisfying some properties. For instance, given the set of all natural numbers N, the relation ≤, which relates two elements x and y if x ≤ y, is a quasiorder on N.
In this work, they define quasiorders on words and use them to construct residual automata. By using different quasiorders we construct different residual automata, including the minimal one for some given language.
Concretely, we present a new residualization operation and a generalized Brzozowski's method for building the minimal residual automaton for a given language. We also leverage this technique to offer a new perspective on NL*, an online learning algorithm for residual automata.
Secret sharing schemes enables a dealer to split a secret into a set of shares, in such a way that certain authorized subsets of shareholders can reconstruct the secret, whereas all unauthorized subsets cannot.
Non-malleable secret sharing schemes (Goyal and Kumar, STOC 2018) additionally require that if the shares have been maliciously modified then the reconstructed secret is completely unrelated one.
The researchers Gianlunca Brian (Sapienza, University of Rome), Antonio Faonio (IMDEA Software Institute), Maciej Obremski (National University of Singapore), Mark Simkin (Aarhus University), Daniele Venturi (Sapienza, University of Rome) have worked jointly to create "Non-Malleable Secret Sharing against Bounded Joint-Tampering Attacks in the Plain Model" paper that was accepted at Crypto 2020.
In their work, they construct non-malleable secret sharing schemes secure against attackers that can maliciously modify the shares more than once in the so-called joint-tampering model.
In particular, assuming one-to-one one-way functions, they obtain:
– A threshold secret sharing scheme secure under attacks where the attacker commits to a partition of the shares, and keeps tampering jointly with the shares within such a partition (so-called selective partitioning).
– A secret sharing scheme for general access structures which tolerates joint tampering with subsets of the shares of size O(√log n), where n is the number of parties. The scheme is secure even if the attacker is allowed to adaptively change the partitions (so-called semi-adaptive partitioning).
Their research lies a new technique showing that every one-time statistically non-malleable secret sharing against joint tampering is in fact leakage-resilient non-malleable (i.e., the attacker can leak jointly from the shares prior to tampering). This may be of independent interest, and in fact they show it implies lower bounds on the share size and randomness complexity of statistically nonmalleable secret sharing against independent tampering.
Research Results
The researcher from the IMDEA Software Institute Pedro Valero, supervised by Pierre Ganty, defended his PhD thesis with the title “On the use of Quasiorders in Formal Language Theory”, on the 20th of July. He submitted his thesis as partial fulfillment of the requirements for the degree of Doctor of Philosophy in Software, Systems and Computing.
Quasiorders on words, i.e. binary relations between words, have proven useful for reasoning about formal languages from a theoretical perspective. For instance they have been used to characterize the class of regular languages and for showing that all maximal solutions of certain systems of inequalities on languages are regular.
In his work, Pedro shows that quasiorders also have practical applications by placing them at the core of several efficient algorithms.
More precisely, in his thesis, Pedro uses quasiorders on words to offer a new perspective on two well-studied problems from Formal Language Theory: deciding language inclusion, with applications to searching on compressed text, and manipulating the finite automata representations of regular languages.
The Language Inclusion Problem
The thesis considers the language inclusion problem L1 ⊆ L2, where L1 is regular or context-free and L2 is regular.This problem is solved by checking whether an over-approximation of L1 is included in L2, showing that the language inclusion problem is decidable whenever the over-approximating function satisfies a completeness condition (i.e. its loss of precision causes no false alarm) and prevents infinite ascending chains (i.e. it guarantees termination of least fixpoint computations).
Such over-approximation of L1 is defined using quasiorder relations on words where the over-approximation gives the language of all words “greater than or equal to” a given input word for that quasiorder. In his thesis, Pedro presents a range of quasiorders in order to systematically design decision procedures for different language inclusion problems such as regular languages into regular languages or into trace sets of one-counter nets and context-free languages into regular languages.
Some of the obtained inclusion checking procedures correspond to well-known algorithms, like the so-called antichains algorithms, while others correspond to novel algorithms such as the presented greatest fixpoint language inclusion check, which relies on quotients of languages.
Searching on Compressed Text
Secondly, the thesis instantiates the quasiorder-based framework for the scenario in which L1 consists on a single word generated by a context-free grammar and L2 is the regular language generated by an automaton. The resulting algorithm can be used for deciding whether a grammar-compressed text contains a match for a regular expression.
This algorithm is then extended in order to count the number of lines in the uncompressed text that contain a match for the regular expression. Remarkably, this extension runs in time linear in the size of the compressed data, which might be exponentially smaller than the uncompressed text.
Furthermore, Pedro's thesis proposes efficient data structures that yield optimal complexity bounds and an implementation –zearch– that outperforms the state of the art, offering up to 40% speedup with respect to highly optimized implementations of the standard decompress and search approach.
Residual Finite-State Automata
The last technical contribution of this thesis is a framework of finite-state automata constructions based on quasiorders over words that provides new insights on residual finite-state automata (RFA for short).
This framework is used to present a generalization of the double-reversal method for RFAs along the lines of the one for deterministic automata and to offer a new perspective on NL∗, an on-line learning algorithm for RFAs. These results evidence that quasiorders are fundamental to residual automata in the same way congruences are fundamental for deterministic automata.
Research Results
The researcher of the IMDEA Software Institute, Pepe Vila, has sucessfully defended his PhD thesis titled: "Learning secrets and models from execution time". Professor Boris Köpf (on leave researcher of the Institute and researcher of Microsoft Research Lab at Cambridge) was his advisor.
In his work he studies some of the problems arising on computer systems that leak information through execution time. They study several instances of how these leaks can be used to both learn secrets—of a confidential computation—and models—of an underlying component—, providing examples that violate previous assumptions about systems’ security or about the attackers’ capabilities.
He studies in particular, time leakage under three different scenarios, providing multiple independent contributions in each of them:
• First, he shows that event-driven software systems are susceptible to side- channel attacks. The key observation is that event loops form a resource that can be shared between mutually distrusting programs. Hence, con- tention of this resource by one program can be observed by the others through variations in the time the latter processes take for dispatching their events. We exploit two different shared event loops in the Chrome web browser, and use the information obtained in three different attacks: for web page fingerprinting, for keystroke detection, and for a cross-origin covert channel.
• Then, he reveals that the contributions are both theoretical and practical. On the theoretical side, we formalize the problem of finding minimal eviction sets, a key primitive for several microarchitectural attacks, and devise novel algorithms that improve the state-of-the-art from quadratic to linear. On the practical side, we perform a rigorous empirical analysis that exhibits the conditions under which our algorithms succeed or fail.
• Finally, he presents a practical end-to-end solution for inferring deterministic cache replacement policies using off-the-shelf techniques for automata learning and program synthesis. The enabling contribution is a chain of two abstractions: a clean interface to the hardware cache replacement poli- cies based on timing measurements on a silicon CPU; and a mapper that exposes a membership oracle to the cache replacement policy abstracting away the details regarding cache content management.
In conclusion, the results of Pepe Vila's thesis constitute an evidence that better models and quantification methods -for both software and hardware systems-, are required in order to reason about the soundness and trade-offs of security countermeasures; and provide a basis for principled countermeasures against, or paths for further improving the efficiency of, several side channel attacks.
The IMDEA Software Institute has been awarded the prize for the best innovative practice in health promotion in the category of small and medium enterprises by the Mutua Universal.
The 5th edition of the Mutua Universal Innovation and Health Awards recognizes innovation for the benefit of people and its awards are intended to distinguish and reward the work of those companies that are highly committed to health promotion and have carried out innovative projects or actions that represent an improvement in the quality of life and health of their workers.
The award-winning action 'IMDEA Software ecoHealth' was born with the approach of the new headquarters of the IMDEA Software Institute in 2009 and since then has been developed and expanded over time, as well as with the invaluable collaboration of its own workers.
The main objectives of the action are: promote ecological awareness; facilitate integration in a multicultural environment; offer possibilities for work-life balance; and maintain a continuous conversation over time on matters of general interest in order to advance and innovate by pursuing constant improvement for the entire staff.
The IMDEA Software Institute provides facilities for its workers to lead healthy lives and exercise: it promotes cycling by providing the car park with its own space; it has a multi-purpose room next to the changing rooms where sports activities can be carried out; it has a breastfeeding room; and, among other things, it is a cardio-protected space that offers its staff training to be able to apply it if necessary.
In addition, the Institute is a research centre committed with the environment. It has parking spaces with electric chargers, 100% ecological cleaning products are used and recycling is actively encouraged, and the automation system turns the building into an efficient space (Energy Class B).
María Alcaraz and Blanca Gutiérrez interview
The researchers Ignacio Cascudo (IMDEA Software Institute) and Bernardo David (IT University of Copenhagen) have recently published "ALBATROSS: publicly AttestabLe BATched Randomness based On Secret Sharing".
ALBATROSS is a family of multiparty randomness generation protocols with guaranteed output delivery and public verification that allows to trade off corruption tolerance for a much improved amortized computational complexity.
Their basic stand alone protocol is based on publicly verifiable secret sharing (PVSS) and is secure under in the random oracle model under the decisional Diffie-Hellman (DDH) hardness assumption. They also address the important issue of constructing Universally Composable randomness beacons (that can be used in more complex environments), showing two UC versions of Albatross: one based on simple UC NIZKs and another one based on novel efficient "designated verifier" homomorphic commitments. Interestingly this latter version can be instantiated from a global random oracle under the weaker Computational Diffie-Hellman (CDH) assumption.
An execution of ALBATROSS with n parties, out of which up to t = (1/2 − ε) · n are corrupt for a constant ε > 0, generates Θ(n^2) uniformly random values, requiring in the worst case an amortized cost per party of Θ(log n) exponentiations per random value. On Cascudo and David paper they significantly improve on the SCRAPE protocol, which required Θ(n^2) exponentiations per party to generate one uni- formly random value. This is mainly achieved via two techniques: first, the use of packed Shamir secret sharing for the PVSS; second, the use of linear t-resilient functions (computed via a Fast Fourier Transform-based algorithm) to improve the randomness extraction.
The main application of these protocols is in proof-of-stake blockchains, which, every certain period of time, requires to elect a "leader" among the users of the protocol, and where this selection must not be possible to be biased, and the correctness of this process needs to be able to be verified publicly.
The IMDEA Software Institute researchers Pepe Vila, Pierre Ganty and Marco Guarnieri, and Boris Koepf, from Microsoft Research, are the authors of the recent paper “CacheQuery: Learning Replacement Policies from Hardware Caches” accepted at the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2020).
Caches are small and fast memories that sit between the CPU and the main memory (DRAM) of computers. Their main goal is to speed up computations by reducing the time it takes to load and store data, and since their capacity is limited, they must anticipate which data is going to be used in the near future. The better this prediction, the better the performance.
Thus, the cache replacement policy is the logic that decides which data is kept in the memory cache and which is replaced to make room for more useful data. It is a critical component for the performance of modern computers.
In most modern processors these policies are not documented, and since they have a huge performance impact, the absence of precise models makes it very difficult to predict and analyze the behavior and security of programs.
“We lack precise models of our hardware. With our approach, we close this gap, and we allow other people to understand how the policy optimizes certain workloads, so that they can predict the timing behavior of critical systems (i.e., cars or planes), calculate limits on the information leakage of cryptographic programs, or write more accurate hardware simulators” comments Pepe Vila, predoctoral researcher of the IMDEA Software Institute.
Transparency, is the first step towards improving the security and safety of computer systems. In this sense, the researcher of the Institute, Marco Guarnieri, says that: “microprocessors and memories are central components of our computing infrastructure. Security vulnerabilities in these components may result in attacks affecting any program running on top of them. To assess and study the security of microprocessors and memories, researchers need high-level models documenting and describing their behaviors. Unfortunately, many crucial details of how these components work are undocumented. We see our research as a first step towards automatically generating such high-level models from hardware measurements and, ultimately, towards more secure systems”.
Through this partnership, the IMDEA Software Institute and BBVA have created a joint framework to research the use of this technology in the development of digital solutions that make it possible to harness data’s potential while also ensuring that users’ data remain private, anonymous and secure.
The agreement is especially relevant in the current context marked by the coronavirus crisis, which is demonstrating the importance of having robust systems to safeguard the privacy and security of data. On the one hand, this is due to the rise of cyber-attacks in recent weeks in which cyber criminals are taking advantage of users’ increased use of digital channels during the lockdown. And on the other, due to the interest sparked by the creation of COVID-19 tracking apps that respect data privacy, for which technologies of this kind could be very useful.
With this new partnership, both institutions will explore the application of a series of cryptographic techniques in the financial sector - techniques that make it possible for data to be shared and analyzed without exposing their content to third parties thanks to algorithms, protocols and encryption systems. These technologies, known as PET, or privacy-enhancing technologies are one of the fields in which the IMDEA Software Institute specializes, as well as one of the areas of interest that BBVA researches in its Research and Patent area.
Within this group of technologies, one that has the greatest potential and which will be the main subject of the new team’s study is zero knowledge proofs (ZKP). This technology uses cryptographic algorithms to make it easier to verify the accuracy of information, without having to share the data that comprise it. This way, it can help to create data-based solutions in which customers’ sensitive data is not exposed to third parties (as it is not necessary to share the data with them to prove that they are accurate).
Thanks to this agreement, both institutions are combining their capacities and knowledge in these areas. The goal is for the research to translate into tangible advances that make it possible to transfer the benefits of this technology to the financial sector, the corporate world, the scientific community and society as a whole.
To do so, in the first stage, the joint team will research how to solve some of the current challenges that the roll-out of this technology is still facing in order to share the results with the scientific community to foster progress in this discipline. Some of these challenges involve its integration with the current communication systems that companies are using, or the lack of common standards for the use of cryptographic protocols, which complicates its adoption on a large scale.
BBVA and the IMDEA Software Institute will also work on a series of real use cases identified in the financial sector, as well as the development of viable prototypes that can be incorporated in the digital products and services offered to BBVA customers.
Joint statement on contact tracking
The pre-doctoral researcher at the IMDEA Software Institute, Pepe Vila, participated at RootedCON 2020 last 7th of March giving a talk titled ‘The '80s never died: automata theory for reversing modern CPUs’ (view presentation). He explained his latest paper developed with the support and of the researchers Pierre Ganty and Marco Guarnieri, from IMDEA Software Institute, and Boris Köpf, from Microsoft Research, 'CacheQuery: Learning Replacement Policies from Hardware Caches' which reveals the previously unknown implementation of cache replacement policies used in modern processors.
Understanding the timing behavior of modern CPUs is crucial for optimizing code and for ensuring timing-related security and safety properties. Unfortunately, the timing behavior of modern processors depends on subtle and poorly documented details of their microarchitecture, which has triggered laborious efforts to reverse-engineer microarchitectural details. Cache replacement policies have received special attention, because they control the content stored in the memory hierarchy and hence heavily influence execution time.
In the paper, which has been accepted into PLDI'20 (Conference on Programming Language Design and Implementation), researchers from the IMDEA Software Institute and Microsoft Research present an end-to-end solution for automatically learning cache replacement policies from hardware time measurements. Their contribution is based on two main contributions: a tool, called CacheQuery, that provides an interface to any set in the cache hierarchy, freeing the user from having to deal with intricate details such as address translation, index mapping, interference from other cache levels or measurement noise; and, an algorithm, called Polka, that provides an abstract automaton for the cache replacement policy, and exploits various symmetries that make the automaton learning techniques applicable to the problem. In addition, they have been able to synthesize programs to automatically derive readable descriptions of the learned replacement policy.
In the experimental phase, their tests have been successful in learning several cache replacement policies used in Intel's latest processors, including two previously undocumented policies.
The 11th of February, on the occasion of the International Day of Woman and Girl in Science, the IMDEA Software Institute organised the conference 'Breaking Codes: Women and Girls in Science' with the support of various researchers from the Institute, as well as other centres on the Campus, such as the Center for Biomedical Technology CTB.
Blanca Gutiérrez, Communication Manager at the IMDEA Software Institute, was in charge of opening the conference in which she explained the importance of research for the advances in society and highlighted the need to promote scientific and research vocations in women and girls in a sector that is mainly masculine.
The first workshop was on reconstruction of neurons. Marta Domínguez and Marta Turégano, researchers at the CTB showed what a neuron is and helped the young women in the audience to differentiate between the different parts of a neuron: synapses, mitochondria, as well as spinal apparatus and myelin sheaths. In addition, they showed the software they use in their laboratory by which it automatically detects each differential element to be studied.
The cryptography workshop was led by three researchers from the IMDEA Software Institute: Anaïs Querol, Elena Gutiérrez and Isabel García. The first to open the workshop was Anaïs, who spoke about the origin of ciphered messages and how to encrypt and decrypt them. On the other hand, Isabel explained how to break mono-alphabetic ciphers. And finally, Elena delved into the workings of the enigma machine and how ciphers were broken at Bletchley Park.
After the workshops, the wikiton began. We divided the audience into groups and gave them a choice between seven Spanish scientists from different fields to create, through information provided, their page on Wikipedia.
The day ended with the 20 questions of the scientific trivial in which the knowledge acquired during the day was tested, as well as the general culture of the public.
The first blockchain hackathon for environmental action in Spain, organized by the IMDEA Software Institute and EIT Digital, whose awards were sponsored by the Tezos Foundation, ends with 11 award-winning participants from the three groups selected by the jury.
ChainrEaction had overall 26 participants, from 10 different countries. 10 of them were university students, 12 master students and 8 doctoral students. Almost 95% of the people respondents have interest (answering yes or maybe) in working at the IMDEA Software Institute. 50% of them punctuated 4 or 5 out of 5 according to their interest in a research-oriented career before chainrEaction, and this figure increased by 22,2% after the hackathon.
Three intensive days that began with presentations, and the introduction to the event given by Blanca Gutiérrez, Communication Manager, as well as Zsolt István, Assistant Research Professor, as part of the chanrEaction organizing committee of the IMDEA Software Institute. The morning continued with an inspiring talk by David Dao, Founder of Forest X, on "Decentralized Sustainability: Beyond the Tragedy of the Commons with Smart Contracts (and AI)".
Daniel Pérez, Chief Technology Officer at the Imperial College London, gave a tutorial on Ethereum as a mentor of chainrEaction that was a valuable, practical and challenging information for participants.
The second talk of the first day was given by Chrysa Stathakopoulou, a chainrEaction mentor and PhD student at ETH Zurich, on how to use and apply blockchain technology in businessess.
Meanwhile, Matteo Campanelli, postdoctoral researcher at the IMDEA Software Institute, organizer of chainrEaction and also a mentor, presented the second tutorial of the day on the chain code of Fabric Hyperledger and websites to interact with it.
During the last part of the day the participants presented their ideas, selected the seven teams that were formed and started coding.
The second day began with an interesting talk by Matej Šima, CEO os Stove Labs, who gave a beginner's guide to SmartContracts through Tezos technology. For the rest of the day participants had the opportunity to code practically the whole day, as well as to listen to the two EIT Digital Student Ambassadors, Renato Pinto and Cristina Ríos.
On the morning of the third day the seven groups were able to finish preparing their sustainable solutions. From 11 to 13 they presented their results to the jury made up of: the director of the IMDEA Software Institute, Manuel Carro; the director of the EIT Digital Co-Location Center, Jesús Contreras; the advisor to the Regional Ministry of Science, Universities and Innovation, Juan Jiménez; representative of the Blockchain Competence Center of Telefónica, María Teresa Nieto; the Head of Blockchain at iecisa, María Salgado; and the CEO of Stove Labs, Matej Šima.
At noon, "Reflections on blockchain at chanirEaction" began, an event opened to the public created within the framework of the hackathon, which featured different perspectives of blockchain through keynote talks given by international experts from industry and academia. Marko Vukolic, from IBM Research, Sara Tucci, from the CEA List Institute, and Jesús Ruiz, from the Spanish blockchain association, Alastria.
After the talks, Manuel Carro, as representative of the chainrEaction jury announced the winners of the three award categories and later proceeded to present the winning innovative ideas to the public.
The winner of the category "Most impressive proof of concept" was DONERO, an idea to give transparency to donations with a very strong focus. The category "Most viable pitch and business model" went to ENERGYCHAIN. A very well developed idea for transactions in the energy market. And finally, the award for "Most surprising use of blockchain" went to TRIPPIO, an idea to increase travel exchange using public transport.
The Director General of Research and Technological Innovation of the Madrid Regional Government, María Luisa Castaño, closed an event marked by the international youth talent that gave everything to create real wonders of sustainable solutions.
Photo Gallery ChainrEaction Website Video playlist
The IMDEA Software Institute and Nomadic Labs have signed a collaboration agreement to conduct research at the highest level in the Institute's research areas with the aim of contributing to the development of the Tezos ecosystem.
The Director General of Research and Technological Innovation of the Madrid Regional Government, María Luisa Castaño, and the Deputy Director of Research, Bárbara Fernández-Revuelta, attended the official signing ceremony between both institutions.
The director of the IMDEA Software Institute, Manuel Carro, the president of Nomadic Labs, Jérôme Chailloux, and the scientific director of Nomadic Labs, Michel Mauny, signed the collaboration agreement that implies that the Institute becomes a strategic partner of the Tezos ecosystem. "The Tezos project has forged numerous scientific collaborations at the best French and international level, as demonstrated by this collaboration with the IMDEA Software Institute. It is very important for us to prepare for the future of blockchain technologies, especially Tezos, by supporting open scientific research, the results of which will be public and therefore benefit the whole community. We are particularly pleased with the signing of this agreement between Nomadic Labs and IMDEA, which strengthens our ties with IMDEA and provides a framework for our collaboration", said Michel Mauny.
Manuel Carro stated that, "the agreement with Nomadic Labs for collaboration in the Tezos environment, the first to be signed in Spain, is an unparallel opportunity to contribute to a technology that is having difficulties to overestimate impact on society".
Photo Gallery Collaboration website
Research Results
The researcher of the IMDEA Software Institute, César Sánchez, talks about the ElasTest project in a video interview published on the Youtube channel of the Institute.
ElasTest is a Project funded by the European Union under the Horizon 2020 program. The main goal of the project is to provide a tool and an infrastructure to test end to end elastic applications. The modern cloud applications back ends are essentially elastic which means that they demand, they consume, they need more resources when they have, for example, more users, more access in the service, so this applications are notoriously difficult to test and to provide a software reliability which is a big challenge for mid-size and small enterprises. The project essentially is building an infrastructure to do this end to end testing and the different circumstances, for example: different users, many users at a time, different browsers, failures in the network and such, even failures in the components on the application itself.
The role of the IMDEA Software Institute in the project ElasTest has been to one, test security in the application and the other is to provide monitoring that allows to describe the test in an easier manner and to assess the test dynamically. César Sánchez ends the interview saying that: “All in all, I think that the ElasTest project has been very successful in both academic and in terms of developing the tool.”
Research results
Micro-architectural attacks, like the recently discovered Spectre and Meltdown attacks, exploit critical vulnerabilities in modern processors to compromise a system's security.
These attacks affect all modern general-purpose processors (such as those used in our computers). Concretely, they can bypass common security defenses at the software level by exploiting hardware side-effects.
In Marco Guarneri’s research, he developed tools for better understanding how micro-architectural attacks work. He then leverages this understanding to design new defense techniques against these attacks.
As a concrete example, Marco Guarnieri, José F. Morales and Andrés Sánchez, from the IMDEA Software Institute, Boris Köpf, from Microsoft Research, and Jan Reineke, from Saarland University recently developed SPECTECTOR, an automated technique for determining whether programs are vulnerable to a specific class of micro-architectural attacks called speculative execution attacks.
“Using Spectector, we detected subtle bugs in the way countermeasures against speculative execution attacks are placed by major compilers. These bugs may result in insecure programs or inefficient programs” ended Marco.
Research results
Niki Vazou, researcher at the IMDEA Software Institute, Martin A.T. Handley and Graham Hutton, from the University of Nottingham, UK have developed “Liquidate your Assets” a paper they presented to POPL2020 . You may find it here.
Liquid Haskell is an extension of Haskell’s Type system that allows annotating types with refinement predicates. It is great for ensuring correctness of code, but it can also be used to improve the performance of code.
Vazou, Handley and Hutton have designed and implement a system that allows Liquid Haskell to be used to formally reason about the resource usage of pure Haskell programs. Moreover, it supports reasoning about correctness and efficiency properties in a combined, uniform manner. "Our system takes the form of a library and requires no modifications or extensions to the compiler" comments Niki Vazou.
They have proven that their library’s approach to cost analysis is correct with respect to an underlying model of execution cost using the metatheory of Liquid Haskell.
In the end, they have demonstrated the applicability of their library on a wide range of case studies, ranging from standard sorting algorithms to sophisticated relational cost properties.
Luca Nizzardo, was a PhD student of the IMDEA Software Institute and his thesis “Cryptographic Techniques for the Security of Cloud and Blockchain Systems” defended in 2018 was directed by the Associate Professor, Dario Fiore. Nowadays he works for Protocol Labs helping to build protocols, systems, and tools to improve how Internet works.
This month the UPM has resolved the two winners of the Extraordinary Award and Luca’s thesis is one of them. In which he investigates how to enforce the honest behavior of parties involved in a digital interaction over the Internet. In particular, considering two emerging paradigms in this setting: Cloud computing and E-commerce.
The Human interactions often involve people who have different and sometimes contrasting interests, like buyers and sellers or consumers and providers. For what regards physical interactions, the society has developed during the years many different ways to protect users against misbehaviors. Nevertheless, when this communication happens in the digital world through the Internet, where people do not meet or even know each other, such a protection is more challenging to obtain, and additional digital tools are needed in order to defend users.
Two main security concerns that have given attention by the research community are those about the privacy and authenticity of the data stored and processed in untrusted environments. Intuitively, for privacy a Client does not want the server to learn any information about the outsourced data. For authenticity, the Client instead wants to be sure that the Cloud computed correctly on the outsourced data.vIn his thesis he focused on this second problem, advancing the study of homomorphic authenticators. In homomorphic authenticators a Client C outsources authenticated data to the Cloud. Later on, a third entity (the Verifier) can ask the Cloud to compute a function f over the Client’s outsourced data. Using a special procedure, the Cloud can provide the Verifier with an authenticator for the output of the function, which allows the Verifier to check the validity of the computation queried.
The contribution of the thesis addresses three different aspects of homomorphic authenticators: definitions, efficiency and functionalities.
First, it introduces a new security model which is stronger and easier to deal with compared with the existing one, along with two compilers which allow one to go from the old model to the new one. Second, it provides the first linearly homomorphic signature scheme whose verification keys have size sublinear in that of the outsourced dataset. Third, it formalizes the notion of homomorphic authenticators for functions which take inputs authenticated using different keys, providing concrete constructions both in the case of private and public verification.
For what regards E-commerce and, more in general, the possibility of transferring value through the Internet, this work is focused on achieving fair exchange by profiting of the Blockchain features, where with fair exchange we mean the possibility for two users to swap digital goods such that neither can cheat the other through Zero Knowledge Contingent Payments (ZKCP) protocol.
Research results
Dario Fiore, Anaïs Querol and Matteo Campanelli, researchers of the IMDEA Software Institute, have talked about the new framework they have developed, called LegoSNARK, which paper was published at the ACM Conference on Computer and Communications Security.
Dario Fiore, Associate Research Professor, started saying that "in our society we often experience a tension between the privacy of our data and the utility of its use. For example, assume that you want to rent a house and the landlord ask you to prove that your monthly income exceeds the rental fee. Now, you would not like to reveal exactly how much you earn because for example this may induce the landlord to increase the price in the future. So, how can you then make this proof and without revealing too much information. Zero-knowledge proofs are a magical cryptographic tool that allows to prove a statement about private data without revealing more information than the fact that the statement is true".
The PhD student, Anaïs Querol started showing a physical example of how it is possible to convince the landlord that you can afford the rent. "Suppose that the rent costs 4 coins and we earn 10 coins. We insert those 10 coins inside this opaque coin dispenser, so by the shape of the dispenser at least you can see that I have 3 coins. How can I prove the landlord that I have at least 1 more? It is very simple, I simply get this one out and now you can see that I have 1,2,3 and 4. So the landlord knows that I can afford the apartment, but they have no clue about our spare money". She ends up saying that this can look quite simple, but in a digital transaction when you have to convince someone on the other side of the world cool mathematical techniques come into play to make it possible!
Matteo Campanelli, post-doctoral researcher, adds that now the emerging technologies like blockchains or cryptocurrencies are pressing out to make all these systems practical. "Recently at IMDEA what we did was tackling two of the main challenges in the space. The two main challenges are one, that these things, the digital analogy of the physical world opaque coin dispensers are very complex and the other is that they are slow. In order to tackle these problems, we develop a framework called LegoSNARK. Basically, we design techniques that allow to construct these systems not in a monolithic way but more modularly. So, think of not a whole piece of clay, but made of different construction blocks of sort, and that’s why we called it LegoSNARK. The interesting thing is that this approach also gives you more efficient zero-knowledge proofs in general".
Scientific results
The pre-doctoral researcher of the IMDEA Software Institute, Pedro Valero, explains the work he has done recently that has taken him to Facebook.
"Technological giants generate vast amounts of information constantly and the only way they have to manage this information efficiently is by compressing it. However, they keep this information because they want to process it later, so saving the information in compressed form means that every time they want to query the information it is necessary to decompress it and perform the search on the original data. We specifically have been working with textual data. In this scenario, when compressing the file you need to find parts of the text that are repeated several times. Then the repeated text is written the first time it occurs and, for the rest of the occurrences, we simply indicate that what comes next is the fragment that appeared previously. This idea allows us to compress the file and save space but it also allows us to speed up the searches because, when we are processing the text, each time we find that what comes next has already occurred before, we can reuse the information we had already obtained when processing that same string of text. This idea is conceptually simple, but we have been among the first ones to put it into practice. We have developed an algorithm that allows us to perform these searches and really saves time.
If the file can be well compressed then the search in the compressed text without decompression can be faster than the whole process of decompressing and searching.
The problem with this approach is that not every compression algorithm works. Only a certain set of algorithms that are known as dictionary algorithms, or grammar-based, are worthwhile, and those algorithms are typically not studied within industry since they are generally slightly slower and more expensive, although they can produce good results.
The work that I have been doing with Facebook is to study this type of algorithms and find out in what context they can be used since, as usual, it is not always convenient to use them, but there are some scenarios in which it is worth to spend a little more time to compress the file in exchange for being able to search faster".
The vice-president of the Community of Madrid, Ignacio Aguado, the Regional Minister of Science, Universities and Innovation, Eduardo Sicilia, and the General Director of Research and Technological Innovation visit the IMDEA Energy Institute to learn about various initiatives against climate change. The political representatives have been received by the directors of the seven IMDEA Institutes.
During the tour through several laboratories, researchers of IMDEA Energy explained several projects in which they participate and, among other things, they highlighted that they have managed to produce kerosene from CO2, water and concentrated solar energy, which constitutes a worldwide milestone that could have important consequences both for long-distance aviation and for the naval sector.
In his speech to the media, Ignacio Aguado stated that "investing in scientific innovation and cutting-edge research programmes is a priority for this Government", which allocates 1.71% of its GDP to R&D activities.
The IMDEA Software Institute also contributes to the climate cause. Computer systems, from data processing centres to personal mobile devices such as smartphones, are major energy consumers. Reducing this consumption without cutting performance is a major challenge with a clear positive impact on the environment. Traditionally, there have been attempts to improve hardware, and currently, the focus is on improving software to perform the same functions with lower energy consumption.
View the photo gallery
Manuel Bravo, Post-doctoral Researcher at the IMDEA Software Institute has proposed elegant algorithms for transaction processing in FARM-like databases, proved their correctness and identified how they should be changed to exploit Remote Direct Memory Access (RDMA), a new networking technology that has the potential to drastically increase the scalability of distributed databases. However, to realize this potential, the algorithms for transaction processing in such databases have to be radically redesigned.
The first industrial database to use RDMA is the recent FARM system from Microsoft, which is now used to compute some of the search queries in Microsoft Bing. Unfortunately, the theoretical foundations of FARM have been shaky: its algorithms have not been proven correct and the rationale many of its design decisions was unclear.
Bravo, that has presented this proposal as a paper to PODC, demonstrates that the methodology for modifying transaction processing algorithms to run over RDMA also opens the door to exploiting RDMA for scaling up other industrial databases. This work has increased confidence in the correctness of FARM design, and allowed proposing its simplifications,
AVERTIS, an event dedicated to Analysis, Verification and Transformation for Declarative Programming and Intelligent Systems, the line of research carried out by our researcher and former director of the IMDEA Software Institute, Manuel Hermenegildo, was held last Friday, November 29th, with a large number of experts in the field.
AVERTIS became an intense and interesting day full of knowledge, scientific dissemination and companionship.
In total, the event had 13 exceptional speakers: Roberto Giacobazzi; Patrik Cousot; Andy King; María García de la Banda; David S. Warren; María Alpuente; Narciso Martí Oliet; Martin Wirsing; Veronica Dahl; Peter Stuckey; Mike Codish; Gopal Gupta; and Ricardo V. Peña Mari.
View the photo gallery.
Speculative execution attacks, such as Spectre, exploit critical vulnerabilities in modern processors to leak sensitive information. Marco Guarnieri, José F. Morales and Andrés Sánchez, from the IMDEA Software Institute, Boris Köpf, from Microsoft Research, and Jan Reineke, from Saarland University, have created Spectector, a tool for proving programs secure against such attacks. The research has been supported by a grant from the Intel Strategic Research Alliance.
Spectector implements the first principled approach for reasoning about the information leaks exploited by Spectre-style attacks. Spectector leverages symbolic execution and self-composition to automatically prove that programs satisfy a property called speculative non-interference, which guarantees the absence of speculative leaks, or detect violations.
Using Spectector, they detected subtle bugs in the way Spectre-countermeasures are placed by several major compilers, which may result in insecure programs or unnecessary countermeasures.
One of the evidences of the tool’s success is that this month the paper has been accepted at the IEEE Symposium on Security and Privacy 2020.
More than 150 high school students attended the activity "The Roots of Software", on the occasion of the Science and Innovation Week, an initiative from the Comunidad de Madrid, coordinated by the Knowledge Foundation Madri+d, aimed at introducing young talents to software research through challenges, games and videos. A different way of disseminating the science of the IMDEA Software Institute, promoting STEM vocations and attracting future promises.
The director of the Institute, Manuel Carro, was in charge of opening the event and welcoming the students. After him, a promotional video was presented. It tells in a direct and impressive way, the work that is done in software research.
Once the video broadcast was over, the pre-doctoral researchers Silvia Sebastián and Pedro Valero, began to tell what they do and quickly moved on to the games that entertained young people for more than two hours.
They taught the students how problems can be solved faster thanks to parallelization, with sums of large numbers in parallel. Several volunteers were invited to go out on the whiteboard and try to solve the equation in the shortest possible time. In addition, they explained that when working in parallel, it is necessary to coordinate the processes (concurrence). In this sense, the students successfully tried to solve the problem of the philosophers' dinner.
Cryptography was also present, Silvia and Pedro hid a report and the attendees had to break the encryption to know its location.
Another themes of the games were formal systems, the turing test to differentiate humans from machines and finally they used the Kahoot tool so that the young people could vote if the people from the images and videos that were shown to them were fruit of an artificial intelligence or human.
View the photo gallery
The Madrid high-speed network for universities and research, REDIMadrid,an iniciative from the Community of Madrid and managed by the IMDEA Software Institute, celebrates its XIV Conference next October 22nd in the Departmental II of the Móstoles Campus of the Rey Juan Carlos University (URJC).
The conference is a meeting point between research institutions and industry for the exchange of ideas and successful experiences on the application of technologies of very high-speed telematic networks.
The programme for the 2019's edition will start at 9:00 and end at 16:30.
The vice-rector of Digitalization and Internationalization of the URJC, Abraham Duarte Muñoz, will be in charge of opening the event in which there will be speakers from REDIMadrid, the URJC, the Universidad Politécnica de Madrid (UPM), UNED, ADVA Optical Networking, Axians, [Palo Alto](palo alto california) and HPE Aruba Iberia.
Blockchain is not a fad, it is a promising technology that has wide applicability. Sustainability is not only a noun; protecting our planet has become a moral obligation. This is why chainrEaction has been created. It is the first hackathon organized by the IMDEA Software Institute y EIT Digital on the use of blockchain technology to develop sustainable solutions for the communities of the future and thus slow down climate change.
ChainrEaction has two main objectives: bring students closer to research and innovation in the area of blockchain; and contribute to the creation of novel solutions for a more sustainable future.
The event will take place from the 3rd to 5th of February 2020 in Madrid, Spain. A maximum of 33 students can attend and to make sure that you can get here, we will provide travel grants. You will enjoy a unique learning and hacking experience, with a program composed of research and industry talks, technical tutorials and ample time for hacking in groups of 3. You will be guided by top researchers from the IMDEA Software Institute and other research institutions.
The key areas of chainrEaction are:
We accept applications from students in Computer Science and related fields, at the BSc, MSc and PhD level. We will select the all-round strongest candidates – blockchain experience is not a must! Applications until the 17th of November 2019 (23:59 UTC) through: https://apply.chainreaction.es/.
The third season of the IMDEA-CSI activity took place last Friday, the 27th of September, on the occasion of the European Researchers' Night coordinated by the Knowledge Foundation, Madri+d.
The IMDEA Software Institute participated one more year, in this occasion, with the representation of the director of the Institute, Manuel Carro and the postdoctoral researcher Matteo Campanelli.
Carro welcomed the nearly 200 young people who attended. He introduced the crime simulation format that was going to be recreated and assured that "today there are no actors, the researchers that you will see are part of the staff of all the IMDEA Institutes and the members of the Police are not only part of the General Direction of the Scientific Police, but everything they will do at the crime scene is the same as they would do in real life". Finally, the director of the Institute ended by making the room aware that science is behind almost everything.
In this occasion the action takes place in a research center. One of its members appears dead in his office and from there the Scientific Police, as well as researchers come into action to collect and analyze evidence from the crime scene.
The researcher Matteo Campanelli talked about privacy during his presentation and how some tools that are sold as secure offer sensitive user information with which many things can be deduced, such as a person's identity. In this sense, he analyzed the Tablet of the corpse and finds an anonymized clinical database that along with other public data on the web, reveals that he had information about the pregnancy of a partner. From which it can be deduced that the victim was blackmailing her.
Once again, in the end thanks to the joint collaboration between investigators and the National Police, the victim was found guilty of the crime.
View the photo gallery.
Today marks the launch of a pilot project, OPENQKD, that will install a test quantum communication infrastructure in several European countries. The IMDEA Software Institute will participate in the recently funded EU project OPENQKD by providing physical infrastructure and the expertise of personnel of the REDIMadrid innitiative, managed by the Institute. The whole consortium is composed by 38 members, 4 of them from Spain.
Classical and quantum communications will jointly ensure the ICT needs of European governments, service industries (e.g. health, finance), businesses and citizens, even in the presence of quantum computers, or other sophisticated algorithmic attacks against public key infrastructures.
The Project mission is the establishment of QKD-based secure communication as a well-accepted, robust and reliable technology instrumental for securing traditional industries and vertical application sectors, and to prepare the deployment of Europe-wide QKD-based infrastructure in future.
The high level objetives are: raising the awareness of the maturity of QKD; working with end-users to test and validate end-to-end security for businesses and industry sectors based on QKD; advancing QKD systems and QKD-based secure-communication solutions to meet market demands in terms of specifications, standards & certification; and finaly, provide several open test facilities to encourage the development of new QKD-based applications by a wide community.
REDIMadrid is deploying a research network over its own infrastructure. The aim is to avoid a hired capacity network, with new dark-fiber laid out and used exclusively for research activities.
In this context, REDIMadrid will facilitate that quantum lambdas can coexist with lambdas of research traffic, so, it will be possible to verify how the solution works in a real environment.
To achieve its ambitious goals, the OPENQKD project will last three years and have a budget of €15 million funded under H2020-EU.2.1.1. This project has received funding from the European Union´s Horizon 2020 research and innovation programme under the grant agreement no. 857156.
View the press release.
The aerospace division of the engineering and technology group (SENER) has received today the Madrid Regional Minister of Education and Research, Mr. Rafael van Grieken, and the General Director of Research and Innovation, Mr. Alejandro Arranz, to present the company activities in the aerospace sector, especially the 'Madrid Flight on Chip' project, partially funded by the Madrid Regional Government and the European Regional Development Fund.
The General Manager of SENER Aerospace, Mr. José Julián Echevarría, and the Business Development and Strategy Manager of SENER Aerospace, Mr. Diego Rodríguez, welcomed the attendees, gave an initial presentation of the work being carried out at SENER, and briefly explained the 'Madrid Flight on Chip' (MFoC) project. Afterwards, there was a tour showcasing some of the main projects and capabilities of SENER in the aerospace sector.
The visit ended with a more in-depth presentation of the MFoC project by the representatives of the partners: SENER (project coordinator), the Carlos III University of Madrid (uc3m), the IMDEA Software Institute, The Reuse Company, Centum Solutions, Genera Tecnologías, and MARM.
The scientific director of IMDEA Software, Manuel Carro, said: "software is playing a predominant role in aerospace technology today. Moving from embedded, intercommunicating, and certified systems to having system-on-chip makes developing their software much more challenging than before". In addition, Carro has declared how important it is for the IMDEA Software Institute to participate in a project of this caliber: "we are very happy to collaborate in MFoC because it gives us exposure to a type of software - -aerospace software- to which we do not normally have access. By its characteristics, we believe it is a class of complex software that performs essential functions and that we see a an opportunity to apply and evolve our capabilities, while still posing an affordable challenge".
Rafael van Grieken, Regional Minister of Education and Research, stated that Madrid is a focus of attraction for companies today but that there is still a need to strengthen business initiatives, particularly based on advanced technologies. "I am convinced that the Madrid Flight On Chip project will impact more satellites, more companies, and many more people on planet Earth than those of us who are here in Madrid and in Spain", concluded Mr. van Grieken.
View the photo gallery of the event and SENER's press release.
Luís Moniz Pereira, NOVA LINCS Researcher, emeritus Professor at DI FCT NOVA, and member of the Board of Trustees and the Scientific Advisory Board of the IMDEA Software Institute, received the National Science Merit Award 2019 from Portugal, on July 8.
Along his career Pereira has been, among other things, the founding president of the Portuguese Association of Artificial Inteligence becoming one of the pioneeers and most outsdanding researchers in Portugal.
The Lisbon Congress Palace hosted the Science 2019 - Science and Technology Summit in Portugalwhere the awards ceremony was held.
Lucas Kuhring and Zsolt István, researchers at the IMDEA Software Institute, will present a demo "I Can't Believe It's Not (Only) Software! Bionic Distributed Storage for Parquet Files" at the 45th International Conference on Very Large Data Bases (VLDB'19) in Los Angeles, USA.
The size of data to be stored and processed as part of data science applications is increasing and leading to bottlenecks and inefficiencies in the datacenter. A way to reduce these bottlenecks is by tailoring the underlying distributed storage solution to the application domain, using resources more efficiently. Lucas and Zsolt have explored this idea in the context of a popular column-oriented storage format used in big data workloads, namely Apache Parquet.
The prototype they have created uses a storage node based on Field Programmable Gate Arrays (FPGAs) that offers high bandwidth data deduplication and, in the future, near data processing for machine learning workloads. The hardware is combined with a software library that allows transparent access to Parquet files.
The demonstration shows that it is possible to implement in-line deduplication without increasing latencies significantly or reducing throughput by relying on the FPGA's dataflow processing model. It also highlights the benefits of implementing the application-specific aspects in a software library instead of FPGA circuits and how this enables, for instance, regular data science frameworks running in Python to access the data on the storage nodes.
Like every year, the IMDEA Software Institute publishes its annual report that summarizes in general terms the activity that has been carried out during that period of time.
2018’s edition not only updates relevant content but also design and structure. These efforts have been made to make the document more visual, compelling and easier to read.
Last year the Institute was composed by 62 researchers from 18 different nationalities, of which, 26 were PhD students.
Madrid Flight on Chip', 'Verification with Liquid Types' and 'Narrowing the data/Compute Gap with Specialized Hardware' are the three research highlights in this report. It also includes the research projects and contracts in which the Institute has been working during 2018 and those that have begun this year.
For more information, please consult the 2018 annual report link to publication.
The pre-doctoral researcher of the IMDEA Software Institute, Pepe Vila, was one of the speakers at RootedCON 2019, which took place from March 28 to 30, in Madrid. More than 2,500 people attended the event born with the purpose of promoting the exchange of knowledge among members of the security community.
In his talk, Vila reviewed some of the background necessary to understand many of the recent attacks against micro-architectures, such as cache side-channel, rowhammer, and attacks based on speculative execution. In addition, he focused on the problem of finding minimal eviction sets: sets of addresses that collide in the cache. And finally, he also showed a functional implementation in WebAssembly to discuss some of its benefits compared to JavaScript.
You can view the full presentation (in Spanish) here
The Madrid Science and Innovation Fair (MXCI) 2019, organised by the Madri+d Knowledge Foundation and IFEMA, in connection with the #STEMadrid initiative, concludes after four intense days and a large number of visitors. The IMDEA Institutes had the privilege of being there with a stand representing four Institutes (networks, energy, nanoscience y materials) on Thursday and Friday, nd three Institutes software, water y food) on Saturday and Sunday.
This days were full of interesting activities dedicated to show visitors the research done by the Institutes as part of an initiative to promote the excellence in science in the Community of Madrid.
The presence of IMDEA Software at the Fair was a great opportunity to disseminate the research being carried out at the Institute, demystify computer science and encourage STEM vocations. More tan four activities were carried out that helped visitors, in a pleasant and attractive way, to understand what software is, how it works internally and where it is located. In this way, as much information as possible was provided for those who had an interest to awaken a vocation and become great talents in the future.
In particular, on Saturday afternoon, the Institutes IMDEA Software and IMDEA Food collaborated with the Spanish National Police to carry out an activity focused on publicizing "The Science that Investigates Crime". Some visitors were able to put themselves in the shoes of the National Police and helped them gathering evidence from the crime scene. These evidence was then given to the researchers that explained how they are able to extract important information that can help the Police solving the crime.
Link to the photo gallery and the video.
IMDEA Software IMDEA Software Institute Faculty Zsolt István was awarded a Marie Skłodowska-Curie Individual Fellowship, for the Project Accelerated Ordering Service for Distributed Ledgers (ACCORD). The project sets out to improve blockchain systems that target Business to Business use-cases and builds on earlier success in the use of specialized hardware to implement distributed algorithms.
Distributed ledgers (DLs), or blockchains, have the potential of transforming the ways individuals and businesses interact by reducing the cost of transactions and the associated delays dramatically. How can this be done? Delegating today’s trusted third party guarantee to a distributed computing network that relies on cryptographic operations and sophisticated distributed consensus algorithms to ensure that transactions are recorded durably and in a tamper-free manner.
The adoption of DLs outside of crypto-currency use cases has been slow for performance reasons. The ACCORD project aims to increase distributed ledger throughput by at least an order of magnitude, while lowering latencies by a similar factor. To achieve this, the focus is on the core component of DL systems, namely, distributed consensus that is used to establish an absolute order of transactions. This ordering operation is one of the main performance bottlenecks in DLs. So, to fully exploit emerging network technologies and to overcome stagnating CPU performance, ACCORD is planning to use hardware acceleration to offload the steps required by the ordering service.
In the end, the foreseen outcome of the ACCORD project is a DL design with performance that allows it to be deployed in use-cases in which DLs are inadequate today as, for example, trading.
This project has received funding from the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie grant agreement No. 842956.
Next February 11, on the occasion of the International Day of Women and Girls in Science, the Montegancedo Campus will host the conference "I+D+M². Women in Montegancedo" organized jointly by the Universidad Politécnica de Madrid, through the Cajal Blue Brain Project and the Ontology Engineering Group, and the IMDEA Software Imstitute. This is a great opportunity to bring science and research closer to girls and adolescents, to encourage STEM vocations and to interact with young researchers as well as with those who have a consecrated career.
Those attending the conference will have the opportunity to meet women researchers with a consolidated career, the research carried out on campus and will discuss the role of women in science. It is undoubtedly a suitable event to resolve all the concerns that arise when deciding on the academic future.
The aim of this conference is to promote the participation of more women in Science, to highlight the difficulties they encounter during their professional careers and to encourage young researchers to start or continue with their scientific careers.
The meeting will take place from 9:00 a.m. to 5:30 p.m. in the auditorium of the Business Centre of the Montegancedo Campus. Attendance at the event is free but registration is required here.
The IMDEA Software Institute, the Universidad Complutense de Madrid (UCM) y la Universidad Politécnica de Madrid (UPM), have been beneficiaries of the Call for R&D Program Activities of the Comunidad de Madrid, thanks to the project "Intelligent Contracts and Scalable Blockchains and Insurance through Verification and Analysis" (BLOQUES-CM), which has a financing of 763,600 euros, by the Comunidad de Madrid with the support of the European Union Structural Investment Funds.
The Research Group aim to address major challenges of systems based on blockchains and smart contracts, which must be solved so that its use is reliable in areas where high levels of security and data integrity can be achieved.
BLOQUES-CM will advance in the state of: the properties of integrity and anonymity, the verification of infrastructures, the testing of blockchains and, in the tests of correction and use of resources.
In this sense, BLOQUES-CM, among other thing, aims to prevent disappearances or the acceptance of incorrect transactions.
Roberto Giacobazzi, affiliate faculty at the IMDEA Software Institute, received a Distinguished Paper award at the flagship conference of Principles of Programming Languages POPL’19, in Cascais, Portugal, for his work, coauthored with Francesco Ranzato, from the University of Padova, and Patrick Cousot, “A²I: Abstract² Interpretation”.
Their article formalizes offline and online meta-abstract interpretation and illustrate this notion with the design of widenings and the decomposition of relational abstract domains to speed-up program analyses. This shows how novel static analyses can be extracted as meta-abstract interpretations to design efficient and precise program analysis algorithms.
In total, three papers by researchers from the IMDEA Software Institute were accepted at POPL’19, supporting once more the high quality of the research performed at the Institute.
The director of IMDEA Software Institute, Manuel Carro @manuel__carro, will be part of the third round table of the event "Innovation and R & D in Emerging Technologies for Digital Transformation", based on research and innovation in Madrid, which is organized by the Information Processing and Telecommunication Center (IPTC) in the ETSI Telecomunicación of the UPM on January 15, 2019.
This event arises with the purpose of reflecting and analyzing the existing models of development and technological, economic and social relationship between the different agents involved in the processes of digital transformation and the progress of key technologies such as: Cloud, IoT, AI, 5G, Big Data and Cybersecurity.
In addition to IMDEA Software Institute, representatives of companies such as NTT Data,Amazon or Santander; industrial associations such as Madrid Foro Empresarial or DigitalES; representatives of national and regional R & D management entities; and experts from the academy belonging to different Technology Centers, such as IMDEA Materials and the Industrial Electronics Center.
Free entry until complete seats. Registration and more information here.
UPM's 6th Technology Innovation workshop took place at the IMDEA Software Institute. As part of its commitment to empower technology advance and innovation, the IMDEA Software Institute collaborated in the organization of UPM's yearly workshop. The workshop feature keynote speakers and a showcase of some of the best ideas presented to the Innovatech Challenge, as well as the award ceremony for the winners of the contest of ideas.
EIT Digital Spain held its Innovation day 2018, with the participation of several keynote speakers and panelists. Manuel Carro, the director of the IMDEA Software Institute, gave a short presentation on innovation from the perspective of a research center: what innovation is and how higher education can be taken advantage of by research centers and the industrial ecosystem to foster innovation.
The Minister of Science, Technology, and Higher Education of Portugal, Mr. Manuel Heitor, visited the IMDEA Software Institute and the EIT Digital Spain node, together with Mr. Raul Azevedo, director of the recently created DTX Digital Transformation CoLab.
Mr. Heitor and Mr. Azevedo discussed potential lines of collaboration between different stakeholders in Portugal and the IMDEA Software Institute and EIT Digital with Manuel Carro and Jesús Contreras, directors of the IMDEA Software Institute and the EIT Digital Spanish node.
Miriam García (now at IST Austria), a former PhD student at the IMDEA Software Institute under the supervision of Pavithra Prabhakar (now at Kansas State University), has been awarded one of the 2016/17 UPM PhD thesis prizes.
There were a total of three awards for thesis defended at the Computer Science School.
IMDEA researcher Zsolt István is one of the ETH Outstanding Doctoral Theses 2018 Award Winners for his PhD Thesis: “Building Distributed Storage with Specialized Hardware”. (Department of Computer Science Award Winners).
IMDEA Software Institute researcher Niki Vazou has been awarded a distinguished paper award at the ACM Sigplan conference Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA) 2018 for the paper “Gradual Liquid Type Inference". The conference awarded 4 distinguished paper awards among 59 accepted papers.
The paper is a collaboration with Éric Tanter (University of Chile) and David Van Horn (University of Maryland) and combines gradual with liquid types to aid program migration and provide better error messages.
EIT Digital, the European KIC on Information Technologies, organized an event on Digital Finance. The event, held at the Co-Location Center of the Madrid Node of EIT Digital, hosted at the IMDEA Software Institute, featured a round table on business financing through Open Banking and talks by invited speakers. In particular, Atos presented OFION, an initiative nurtured under the umbrella of a innovation and transference activity partially funded by EIT Digital that offers a technological solution to implement flexible invoice factoring in SMEs.
IMDEA Software Institute student Platon Kotzias and researcher Juan Caballero have been awarded a distinguished paper award at the SIGCOMM Internet Measurement Conference (IMC) 2018 for the paper “Coming of Age: A Longitudinal Study of TLS Deployment”. The conference awarded 3 distinguished paper awards among 43 accepted papers out of 174 paper submissions.
The paper is a collaboration with researchers Abbas Razaghpanah (Stony Brook University), Johanna Amann (ICSI/Corelight/LBNL), Kenneth G. Paterson (Royal Holloway, University of London), and Narseo Vallina-Rodriguez (IMDEA Networks / International Computer Science Institute).
Lambda World is a conference aiming to scale the usage of the research achievements in the area of functional programming over the last 40 years in the industrial setting. Aleks Nanevski and Anton Trunov have tried to push it even further, showcasing modern technology, like proof assistants, built on top of dependent types. This approach is highly desirable in the branches of industry needing high assurance guarantees. Anton delivered a workshop on programming in Coq aiming at software developers. And Aleks presented a talk on proof automation using Coq’s canonical structures.
Manuel Carro, director of the IMDEA Software Institute, will be interviewed in the Spanish National Radio (RNE) program “Por tres razones” (For Three Reasons) on Friday, September 28th.
The program runs from 19:00 to 19:45, and will be made available on the website of the program.
Researchers from other IMDEA Institutes and the Director General for Universities of the Comunidad de Madrid will take part in the program as well.
The IMDEA Software institute hosted the third International Workshop on Dynamic Software Documentation (DySDoc3), and the pre-reception of the 34th International Conference on Software Maintenance and Evolution (ICSME) with talks by Bitergia, CQSE and Sourced.
Manuel Carro, the director of the IMDEA Software Institute, contributed again to the Spanish podcast “1BIT de memoria”, focused on the life and achievements of great computer scientists, specifically Turing prize award recipients.
This time, the podcast focused on Leslie Lamport, widely known for his contributions to concurrent and distributed systems, verification, and for being the creator of LaTeX, one of the systems for document preparation most widely used in scientific and technical environments.
IMDEA Software Institute researcher Alexey Gotsman, along with Gregory Chockler (Royal Holloway, University of London), has received a best paper award at the International Symposium on Distributed Computing (DISC 2018). The award was given for the paper “Multi-shot distributed transaction commit”.
IMDEA Software Institute PhD student Pepe Vila discovered a vulnerability in Google Chrome (CVE-2018-16075) that allowed any local HTML file to steal cookies and content from arbitrary domains. This issue has been patched in version 69.
IMDEA Software Institute researchers have presented several papers at the 34th International Conference on Logic Programming (ICLP'18), that this year was a part of the Federated Logic Conference (FLoC'18), held July 14-17, 2018, in Oxford, UK. FLoC is a major event celebrated once every four years which gathers all the major conferences related to logic and computer science. ICLP is the top international venue in the area of Logic Programming and is part of FLoC.
IMDEA Software Institute director Manuel Carro was a member of the Program Committee of ICLP this year. PhD student Joaquin Arias presented s(CASP), a system developed in collaboration with Manuel Carro and researchers from the University of Texas at Dallas. s(CASP) evaluates non-monotonic programs with constraints avoiding the combinatorial explosion due to the grounding phase. The paper entitled "Constraint Answer Set Programming without Grounding", to be published in Theory and Practice of Logic Programming, describes this novel execution model and shows through several examples the enhanced expressiveness of s(CASP) w.r.t. ASP, CLP, and other CASP systems.
PhD student Maximiliano Klemen presented a technical communication on his work with recent PhD graduate Nataliia Stulova, and IMDEA Software faculty members Jose F. Morales, Pedro Lopez-Garcia, and Manuel Hermenegildo, entitled "Towards Static Performance Guarantees for Programs with Run-time Checks". This work presents a framework for reasoning statically about the overhead added to programs by run-time checks in terms of both algorithmic complexity and actual cost changes. Moreover, the framework allows programmers to specify an "admissible" overhead level per program routine (function, predicate, etc.), and automatically and statically check whether the program with run-time checks adheres to such specification for all possible executions.
PhD student Isabel Garcia presented a technical communication on her work with IMDEA Software faculty members Jose F. Morales and Manuel Hermenegildo, entitled "Towards Incremental and Modular Context-sensitive Analysis". This work tackles the issue of the high cost of context-sensitive static analysis on large code bases during the development process. The authors present an approach that combines fine-grain incrementality and modularity, which was not covered by previous approaches. Analysis results are updated at the particular places where the changes to the code are introduced (incrementality), which is significantly less costly than performing global system-level analysis. Local updates are propagated as necessary to the affected program units (modularity), obtaining the same results as standard modular global analysis with greatly reduced cost.
Faculty member Pedro Lopez-Garcia presented his work with PhD student Maximiliano Klemen, recent PhD graduate Umer Liqat, and faculty member Manuel Hermenegildo, entitled "A General Equational Framework for Static Profiling of Parametric Resource Usage" at the 19th Workshop on Logic and Computational Complexity (LCC'18). This novel framework for setting up cost relations can be instantiated for performing a wide range of resource usage analyses, including both static profiling of accumulated cost and the inference of standard notions of cost. This allows identifying statically the parts of programs that have the greatest impact on the total cost.
The IMDEA Software Institute has published its 2017 Annual Report.
Leaving their usual attachment to well-proven technologies and procedures, banking is embracing AI at all levels, from the interaction with clients to their core business.
This trend opens new problems and opportunities in a very powerful sector extremely relevant for our everyday life.
Not only that: the future relationship of banking and AI can shape the role of banking in the society, and how banking deploys their internal processes.
This was the main topic of a panel held on June 22, 2018, by the El Español digital newspaper.
In this meeting, several experts, namely Miquel Moya (Google), Javier Gonzalez Dominguez (Digital Innovation and Big Data, Evo Banco), Rodrigo Miranda (ISDI), Javier Iglesias (Salesforce Iberia), Manuel Carro (UPM and IMDEA Software), and Giorgio Semenzato (Finizens), exchanged their opinions on the solutions that AI can bring to baking and the challenges that this adoption can bring about.
An innovative application of AI in the form of a voice-driven interface adopted by EVO Banco was used to showcase possible application fields.
Former IMDEA Software Institute intern Anaïs Querol Cruz has been selected as a recipient of a prestigious fellowship from “La Caixa” Foundation to carry out a PhD at our Institute. This was the outcome of a competitive selection process that awarded only 20 fellowships out of 602 evaluated applications.
More information here
IMDEA Software Institute recent PhD graduate Luca Nizzardo gave an invited talk at an event on blockchain and cryto values organized by Codemotion in Milan, Italy. The title of Luca's talk was “Bitcoin and Beyond(?), a Cryptographic point of view”.
IMDEA Software Institute faculty member Dario Fiore, together with postdoctoral researchers Antonio Faonio and Matteo Campanelli and other members of the Spanish cryptography community, participated in the presentation ceremony of the 10th BBVA Foundation Frontiers of Knowledge Awards. The ceremony was held at the Marqués de Salamanca Palace of Madrid.
This year the BBVA Foundation gave fourteen awards covering eight categories: basic sciences, biomedicine, climate change, ecology and conservation biology, information and communication technologies, economics finance and management, development cooperation, and contemporary music.
This year's award in the information and communication technologies category is specially relevant for the IMDEA Software Institute. It was given to professors Shafi Goldwasser, Silvio Micali, and Ronald Rivest from the MIT, and to professor Adi Shamir from the Weizmann Institute of Science for their “fundamental contributions to modern cryptology, an area of a tremendous impact on our everyday life”. Cryptography is one of the strongest areas of the IMDEA Software Institute, and we want to take this occasion to warmheartedly congratulate these four outstanding scientists for their achievements and well-deserved recognition.
IMDEA Software Institute researcher and deputy director Juan Caballero gives an invited talk at the 1st OPTICS2 Workshop on Avionics Cybersecurity on June 5-6 in Cologne, Germany. The workshop was organized by the European project OPTICS2. Juan delivered a talk on the evolution of malware network communications titled “A Lustrum of Malware Network Communication: Evolution and Insights”.
PhD students Nataliia Stulova and Luca Nizzardo successfully defended their PhD theses. On May 23, Nataliia defended her thesis entitled “Improving Run-time Checking in Dynamic Programming Languages” and advised by IMDEA researchers José Francisco Morales and Manuel Hermenegildo. On May 24, Luca defended his thesis entitled “Cryptographic Techniques for the Security of Cloud and Blockchain Systems” advised by IMDEA researcher Dario Fiore.
Both Nataliia and Luca obtained their degree from the Technical U. of Madrid (UPM) within the DSS doctoral program, in which IMDEA faculty collaborate.
Pictures of the defense of Nataliia and Luca:
The Tezos Foundation is establishing a multi-year research, training, and dissemination program with IMDEA Software Institute to address Tezos-related technologies including cryptography, computer security, formal verification, distributed systems, and programming languages.
IMDEA's program will focus on the technology surrounding the Tezos cryptographic ledger and smart contracts, which will help advance developments in privacy, correctness, robustness, and scalability. The Tezos Foundation will also offer support to IMDEA's successful Master's/PhD program with the Technical University of Madrid to provide additional focus and research on topics related to Tezos.
Relevant Links:
The team of the MATHADOR project (led by Aleks Nanevski) is pleased to announce the first release of the FCSL-PCM library. FCSL-PCM is a part of Fine-grained Concurrent Separation Logic framework, more information is available at https://software.imdea.org/fcsl/. The source code can be found at https://github.com/imdea-software/fcsl-pcm.
The student Matías Spatz from the German School has joined the IMDEA Software Institute for an educational stay for a period of two weeks. Matias will be supervised by Dr. Juan Caballero who works on the area of cybersecurity.
IMDEA Software collaborates with the German School in its educational stay program for secondary school students. The goal of these educational stays is for students to learn first hand how a company or research center works, as well as their techniques and working approach. These stays at the IMDEA Software Institute will provide a practical complement to the studies, offer a view of the life of a researcher in computer science, ease the integration into the job market, and help to disseminate science among young students.
IMDEA Software Institute researcher Pierre Ganty was invited speaker at the International Workshop on Synthesis of Complex Parameters part of the European Joint Conferences on Theory and Practice of Software.
IMDEA Software Institute Phd student Luca Nizzardo was a panel member for an event on crytocurrencies organized at the University of Milano Bicocca. He served on the panel as an expert on the crytographic aspects of cryptocurrencies.
Next Wednesday, February 7 at 16:00, a round table will be held in the IMDEA Software Institute's auditorium to contribute to the International Day of the Woman and the Girl in Science. This event is celebrated around the world on February 11 and its goal is to achieve full and equal participation in science for women and girls. The round table, moderated by journalist María José Bosch, will be recorded live, and it will be broadcast on Friday, February 9, in the second part of Gestiona Radio's program "Primera Hora" (from 11:00 to 12:00).
Two researchers from IMDEA Software (Alessandra Gorla and Isabel García Contreras) and three invited professors and researchers from other institutions will participate: Ernestina Menasalvas, professor at E.T.S. of Computer Engineers of the UPM; Asunción Santamaría, professor at the E.T.S. of Telecommunication Engineers of the same University; and Elena González-Blanco, General Manager for Europe at CoverWallet and Principal Investigator of the POSTDATA ERC project.
With this round table, open to the public, IMDEA Software joins similar activities organized by the seven IMDEA Institutes with the support of the MadrI+D Foundation and the Ministry of Education and Research of the Community of Madrid.
Links of interests:
Manuel Hermenegildo, Distinguished Professor at the IMDEA Software Institute, has been appointed Chairman of the Scientific Board of INRIA, the French Institute for Research in Computer Science and Automation (Institut national de recherche en informatique et en automatique). He succeeds Professor Kurt Mehlhorn, director at the Max Planck Institute for Informatics, who held the position from 2015.
INRIA is a French national public research institution focusing on computer science and applied mathematics. It comprises 8 research centers (in Bordeaux, Grenoble-Inovallée, Lille, Nancy, Paris-Rocquencourt, Rennes, Saclay, and Sophia Antipolis) and employs 3800 people, including 1300 researchers, 1000 Ph.D. students, and 500 postdocs.
The INRIA Scientific Board provides guidance on the major aspects of INRIA's scientific policy, including the development of the research centers and teams, and the appointment and renewal of directors, in agreement with the Board of Directors.
Professor Roberto Giacobazzi of the University of Verona, Italy and IMDEA Software Institute visiting faculty member is hosting a Shonan Meeting on Intensional and extensional aspects of computation: From computability and complexity to program analysis and security. The meeting takes place at the Shonan Village Center, Japan, January 22–25.
Professor Roberto Giacobazzi of the University of Verona, Italy and IMDEA Software Institute visiting faculty member gives a tutorial on Code Obfuscation at the Tutorial Fest of the ACM Symposium on Principles of Programming Languages (POPL), a flagship conference in this area.
Former PhD student Goran Doychev receives the “Premio Extraordinario de Tesis Doctorales” de la ETS de Ingenieros Informaticos from the Technical University of Madrid (UPM), Spain for the 2015‐2016 course.
Goran's thesis "Tools for the Evaluation and Choice of Countermeasures against Side-Channel Attacks" was supervised by IMDEA Software Institute faculty member Boris Köpf. His thesis focuses on the development of tools to support designers and implementers at the time of choosing the best countermeasures to avoid information leakage through side channels during the execution of cryptographic protocols.
The Spanish speaking podcast “1BIT of memoria” featured IMDEA software researcher Juan José Moreno as their main guest.
Link to the podcast episode.
IMDEA Software Institute researcher Dario Fiore gives a keynote at the Nordic Conference on Secure IT Systems NordSec2017 who took place November 8-10 in Tartu, Estonia. Dario delivered a keynote entitled “Homomorphic Authentication for Computing Securely on Untrusted Machines”.
Professor Roberto Giacobazzi of the University of Verona, Italy and IMDEA Software Institute visiting faculty member gave a talk at the Fall Days on System and Software Analysis held in Nunspeet, the Netherlands, November 6-10.
Roberto's talk is entitled “Securing Code — Hacking the precision of program analysis” and concerns the design of code protecting transformations for anti reverse engineering applications.
In their opening episode, the spanish speaking podcast “1BIT of memoria” featured IMDEA software director Manuel Carro as their main guest.
Link to the podcast episode.
Juan Caballero, Associate Research Professor & Deputy Director at the IMDEA Software Institute, gave an invited talk at Cybersecurity with the Best, the World's biggest cybersecurity online conference for developers. Cybersecurity with the Best was held online on October 14-15, 2017. It comprised of over 40 talks by renowned international cybersecurity experts. Dr. Caballero's talk was titled "The Rise of Potentially Unwanted Programs: Measuring its Prevalence, Distribution through Pay-per-Install Services, and Economics" and it described recent research performed by his group at the IMDEA Software Institute, in collaboration with Symantec Research, on potentially unwanted programs (PUP), a class of undesirable programs that affects a large number of Internet users.
IMDEA researcher John Gallagher will be the program chair of the following events.
The European Researchers' Night and the related activities to be developed in Madrid were the main topics of the interview done to Manuel Carro, professor at the Technical University of Madrid (UPM), Spain, and director of the IMDEA Software Institute by the National TV program La Tarde en 24 Horas. Many research institutions and universities based on the Madrid region will bring researchers and their work closer to the society through almost 40 activities coordinated by the Fundación para el Conocimiento madrimasd next September 29th.
The seven IMDEA Institutes of the Madrid region will jointly present, with the support of the National Police, how science and technology help solving a crime and finding the criminal and its motivation. All of this will take place at the Residencia de Estudiantes on Friday September 29th, from 6pm to 9pm.
Researcher Carolina Inés Dania and Marina Egea (Minsait (by Indra)) win 2017 Best Paper Award for the article "SQL-PL4OCL: An automatic Code Generator from OCL to SQL Procedural Language” published in the Journal of Software and Systems Modeling and presented at the conference MoDELS 2017, Austin, Texas, USA.
The paper, available here, introduces a SQL-PL code generator for OCL expressions that, in contrast to other proposals, is able to map OCL iterate and iterator expressions thanks to our use of stored procedures. Moreover, the proposed mapping can target several relational database management systems.
This edition of MoDELS took place in Austin, Texas, United States from August 28 - September 1, 2017.
Roberto Costumero, student at the Software, Systems and Computation PhD. program, has successfully presented his PhD. Thesis entitled “Big Medical Text Analytics: Querying, Searching and Understanding Clinical Data” to the committee last Wednesday 20th, September. Although Roberto’s research has not been directly performed as a member of IMDEA, he has been also giving shape to the industrial part of his thesis as he is also a member of our community in EIT Digital CLC as a student of the Doctoral School, being the first student in Madrid node to be earning his PhD. Roberto has just started his Business Development Experience for 6 months at Sanitas, in which he will be able to deliver the background of his thesis to the industry.
The Board of Trustees of IMDEA Software Institute has appointed Juan Caballero as new Deputy Director of the Institute. Dr. Caballero obtained his Ph.D from Carnegie Mellon University (USA) in 2010. He joined IMDEA Software as an Assistant Research Professor in November 2010 and was promoted to Associate Research Professor on December 2016.
The IMDEA Institutes participated in the radio show Primera Hora, hosted by Javier García Mateo in Gestiona Radio. During one hour, they spoke about science in general and, in particular, about the science they will show in an upcoming event in CSIC's Residencia de Estudiantes on the evening of September 29th. On that date, and together with members of the National Police, they will present "IMDEA-CSI: crime scene investigation", one of the activities to take place in Madrid as part of the European Researchers' Night in Madrid 2017, coordinated by the Foundation for Knowledge madrimasd.
The members of the IMDEA Institutes who participated were Juan Manuel Ortiz, from IMDEA Water; Ana Ramírez de Molina, from IMDEA Food; Rebeca Marcilla, from IMDEA Energy; Juan José Vilatela, from IMDEA Materials; Álvaro Somoza, from IMDEA Nanoscience; Antonio Fernández Anta, from IMDEA Networks; and Juan Caballero and Manuel Carro, from IMDEA Software.
A recording of the program can be found here.
Boris Köpf, researcher at the IMDEA Software Institute, has participated in the paner entitled "Formal Methods for Reliable Software Security" at the final event of the DFG priority program Reliably Secure Software Systems (RS3) that has taken place in Darmstadt, Germany, from the 4 to the 6 of September.
Alessandra Gorla, researcher at the IMDEA Software Institute, has been invited speaker at the 2nd International Workshop on App Market Analytics celebrated in Paderborn, Germany, on the 5th of September. Alessandra's talk, entitled "Mining the Google Play for Anomalies" presented several analysis techniques to identify anomalous Android applications, such as anomalies that involve mismatches between the description and the implementation, anomalies in the use of sensitive information, and anomalies in the user interface.
Researchers of the IMDEA Software Institute have given several talks at the 33rd International Conference on Logic Programming (ICLP'17), that was co-located with the 23rd International Conference on Principles and Practice of Constraint Programming (CP'17), and the 20th International Conference on Theory and Applications of Satisfiability Testing (SAT'17), held on August 28 - September 1, 2017, in Melbourne, Australia. ICLP is the top international venue in the area of Logic Programming.
IMDEA Software Institute’s faculty members Manuel Carro and Manuel Hermenegildo were members of the Program Committee.
Manuel Hermenegildo gave, jointly with Pascal Van Hentenryck, a plenary ICLP/CP/SAT talk dedicated to the work of Alain Colmerauer, the creator of the Prolog programming language and one of the founders of the field of constraint programming, who passed away this spring.
Nataliia Stulova presented at ICLP'17 her joint paper with José Francisco Morales y Manuel Hermenegildo entitled "Towards Run-time Checks Simplification via Term Hiding", that presents a novel approach for reducing the overhead of some run-time verification techniques by several orders of magnitude based on considering the term visibility rules prior to instrumenting a program with run-time checks.
The 15th International Colloquium on Implementation of Constraint and LOgic Programming Systems (CICLOPS'17), also co-located with ICLP/CP/SAT, was co-organized by Nataliia Stulova y José Francisco Morales, who also chaired it.
Nataliia Stulova also presented a description of her dissertation research entitled "On Improving Run-time Checking in Dynamic Languages" at the ICLP/CP/SAT Doctoral Program that will be published in the ICLP'17 Technical Communications OASIcs series (volume 58), published by Dagstuhl.
Finally, and as reported in separate news, Pedro López-Garcíagave an invited talk at CICLOPS'17 and Pedro López-García and Manuel Hermenegildogave an invited talk at ICLP'17, on occasion of the 10 year Test of Time Award received for their paper entitled "User-Definable Resource Bounds Analysis for Logic Programs".
IMDEA Software Institute's faculty members Pedro López-García and Manuel Hermenegildohave given a plenary invited talk at the 33rd International Conference on Logic Programming (ICLP'17, the premier conference in the area) on their paper "User-Definable Resource Bounds Analysis for Logic Programs", which received the "Test of Time" award as a recognition of the paper published 10 years ago that has had the largest impact. The talk described the contributions of the paper, its applications, and how it has been improved, extended, and generalized over the last 10 years, as well as a summary of its impact in other work.
This edition of ICLP was co-located with international top conferences CP'17, and SAT'17 in Melbourne, Australia, August 28 - September 1, 2017.
IMDEA Software Institute faculty member Pedro López-Garcíagave an invited talk on August 28 at the 15th International Colloquium on Implementation of Constraint and LOgic Programming Systems, CICLOPS'17, in Melbourne, Australia, as part of the joint international top conferences ICLP'17, CP'17, and SAT'17.
Pedro's talk, entitled "Static Profiling of Parametric Resource Usage as a Valuable Aid for Hot-spot Detection," presents a novel technique that allows performing better software optimizations, and in a more efficient way, than the ones obtained with current cost analysis tools.
IMDEA Software Institute researcher Boris Köpf, has chaired the Program Committee of the 30th IEEE Computer Security Foundations Symposium (CSF 2017) together with Steve Chong from Harvard University.
The selected program can be found here.
The conference was held August 21-25, 2017 in Santa Barbara, CA, USA.
The Computer Security Foundations Symposium is an annual conference for researchers in computer security.
CSF seeks contributions on foundational aspects of computer security as well as their application to practice.
PhD student Pepe Vila and researcher Boris Köpf received a distinguished paper award at the 2017 USENIX Security Symposium, one of the top 4 conferences in the area, for their research paper entitled “Loophole: Timing Attacks on Shared Event Loops in Chrome”.
IMDEA Software Institute Researcher, Manuel Hermenegildo, co-organizes and chairs the 4th Workshop on Horn Clauses for Verification and Synthesis (HCVS 2017). The workshop is held on August 7, 2017 in Gothenburg, Sweden, as a satellite workshop of the International Conference on Automated Deduction, CADE 2017.
This series of workshops focuses on Horn clause-based analysis, verification, and synthesis, bringing together researchers working in the communities of Program Verification (e.g., CAV, TACAS, and VMCAI), Constraint/Logic Programming (e.g., ICLP and CP), and Automated Deduction (e.g., CADE).
PhD students Miriam García y Germán Delbianco graduated during the past month. Both students obtained their degree from the Technical U. of Madrid (UPM) within the DSS doctoral program, in which IMDEA faculty collaborate.
Miriam defended her thesis "An Algorithmic Approach for Stability Verification of Hybrid Systems", advised by the former IMDEA researcher Pavithra Prabhakar. This work proposes a novel algorithmic approach to stability verification of hybrid systems, which uses formal methods.
Germán's thesis "Tools for the Evaluation and Choice of Countermeasures against Side-Channel Attacks", was supervised by IMDEA Software Institute researcher Aleks Nanevski. The main goal of the thesis is the development and application of program logics aimed at the modular verification of stateful programs with higher-order control effects.
IMDEA Software Institute Researchers Gilles Barthe and Manuel Hermenegildo participanted in the Dagstuhl Seminar on Resource Bound Analysis, held in Schloss Dagstuhl, Germany, July 16-21, 2017. This meeting brought together the main researchers in the areas of symbolic bound analysis and worst-case execution time (WCET) analysis to discuss the state of the art and future research directions in this important area: the quality of software crucially depends on the amount of resources – such as time, memory, or energy – that are required for its execution. Understanding and bounding resource usage is not only crucial for writing efficient software but also to ensure correctness and safety of software systems, as well as their resilience to attack. Manuel Hermenegildo, jointly with Pedro López-García, Maximiliano Klemen, and Umer Liqat gave a tutorial on Cost Analysis with Recurrence Relations (using CiaoPP) and its Applications and presented their recent work on Energy Consumption Analysis and Verification, also using their CiaoPP tool. The group of Gilles Barthe presented their recent work on Relational Cost Analysis (with Ezgi Cicek, Marco Gaboardi, Deepak Garg, and Jan Hoffmann).
IMDEA Software Institute researcher Juan Caballero, graduated Ph.D. student Antonio Nappa, and former intern M. Zubair Rafique have received the Most Influential DIMVA paper 2009-2013 Award for their paper "Driving in the Cloud: An Analysis of Drive-by Download Operations and Abuse Reporting". The award recognizes the most influential paper published in a period of 5 years at DIMVA, the International Conference on Detection of Intrusions and Malware & Vulnerability Assessment. The authors received their award at the gala dinner of DIMVA 2017, which was held on July 6-7 2017 in Bonn, Germany.
The winning paper was published in DIMVA 2013. It proposed a technique to identify exploit servers managed by the same organization. Exploit servers are Web servers that try to exploit vulnerabilities in the browser and browser plugins (e.g., PDF or Flash players) of visitors. If exploitation is successful, malware is installed on the visitor's computer. This process is known as a drive-by download. In the drive-by ecosystem many exploit servers run the same exploit kit software and it is a challenge understanding whether the exploit server is part of a larger operation. The paper results revealed that although individual exploit servers have a short median lifetime of a few hours, attackers were able to sustain long-lived malware distribution by turning to the cloud, hosting their exploit servers in specialized cloud hosting services.
As a result of the paper the authors released the Malicia dataset, which comprised 11688 malware binaries collected from 500 drive-by download servers over a period of 11 months, a database that details when and from where the malware was collected, and the malware classification into families. The dataset enables, among other applications, evaluating malware clustering and labeling approaches. Since its release, the Malicia dataset has been requested by 73 research institutions worlwide.
Carolina Inés Dania defended his PhD thesis “Mapping OCL as a Query and Constraint Language” advised by IMDEA Software Institute former faculty member Manuel Clavel and Marina Egea.
IMDEA Software Institute researcher Dario Fiore gives an invited talk at the MathCrypt event part of the NIMS Hot Topics Workshop that took place in Daejon, Korea, 29-30 June. Dario's talk, entitled “Computing on Encrypted Data”, presents his work about how to secure computations performed remotely on data stored at an untrusted server. More information about this line of research on Dario's website.
IMDEA Software Institute researcher Carmela Troncoso has participated in the ISSS EU-Datenschutzgrundverordnung und nues CH-DSG organized by the Information Security Society Switzerland in Zurich, Suiza. Her talk, entitled “Systematic Privacy by Design engineering.” explained how to tackle the system engineering problem from a privacy point of view, describing means to reason about embedding strong privacy guarantees into ICT systems, and means to approach the evaluation of private information leakage in such scenarios.
IMDEA Software Institute faculty members Pedro López-García and Manuel Hermenegildo are, with co-authors Jorge Navas (SRI) and Edison Mera (PDC), the recipients of the 10 year Test of Time Award at the 33rd International Conference on Logic Programming (ICLP 2017), the premier conference in the area, for their paper "User-Definable Resource Bounds Analysis for Logic Programs", published in ICLP 2007. The 10 year Test of Time Award recognizes the paper published 10 years ago which has had the largest impact.
The winning paper by Navas, Mera, López-García, and Hermenegildo proposed and developed a technique that allows programmers to implement analysis and verification tools for a very wide class of resources (including execution time, energy consumption, and other user-defined quantitative properties) in a straightforward way, by just defining these resources and other parameters through simple program annotations. The program together with these annotations and resource specifications constitute the input to a customizable analyzer (implemented within the CiaoPP tool) which automatically, and without running the program, predicts the usage of the resources defined in order to guarantee that the program's resource usage will be within the specified limits.
Since its proposal in 2007 the approach and its implementation in CiaoPP have been applied by different groups for computing upper and lower bound functions on resources such as memory consumption, execution time, or energy, for a wide variety of programming languages, ranging from high-level source to bytecode and to machine code. It has also been improved, extended, and generalized in several ways over the last 10 years.
Faculty member Juan Caballero and Ph.D.student Platon Kotzias Platon Kotzias have a paper at the 36th IEEE Symposium on Security and Privacy, a top-ranked conference held in San Jose, CA. The paper was in collaboration with Chaz Lever and Manos Antonakakis from Georgia Institute of Technology and Davide Balzarotti from Eurecom, France. The work, that can be found here, performs a large-scale analysis of malware network communication using 26.8 million malware samples in combination with over 5 billion DNS queries collected from a large North American internet service provider (ISP). Among other, they discover that domains contacted from malware are observed in ISP network traffic often weeks or months before the malware shows up in the malware feeds. They also show that potentially unwanted programs (PUPs) rely on a surprisingly stable DNS and IP infrastructure.
The paper has been recently presented at the 40th M3AAWG General Meeting in Lisbon on June 15th.
IMDEA researcher Juan Caballero will be giving a talk at the 40th M3AAWG General Meeting in Lisbon on June 13th. The Messaging, Malware, Mobile, Anti-Abuse Working Group (M3AAWG) is the largest industry association working against botnets, malware, spam, viruses, DoS attacks and other abuse. It comprises over 200 companies including (among many others): Apple, AT&T, Comcast, Facebook, Google, LaCaixa, LinkedIn, Microsoft, Orange, and Yahoo.
This year the European Research Concil (ERC) celebrates its 10th anniversary. Fundación Madri+d para el conocimiento organizes is celebrating the event in Madrid on June 12, where two ERC grantees (Alexey Gotsman and Aleks Nanevski) from IMDEA Software Institute are taking an active role.
IMDEA Software Institute researcher Carmela Troncoso receives the Best Reviewer Award at the IEEE Security and Privacy Symposium 2017, the flagship conference of the field.
The IMDEA Software Institute is currently involved in the organization of two Summer Schools:
Gilles Barthe co-organizes ProbProgSchool 2017, a summer school on probabilistic programming in Braga, Portugal.
Carmela Troncoso co-organizes the Summer School on Real-World Crypto and Privacy in Sibenik, Croatia.
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.
IMDEA Software Institute researcher Gilles Barthe was keynote speaker at EUROCRYPT 2017 in Paris, France. EUROCRYPT is the second most prestigious venue for cryptography research.
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.
"This project has received funding from the European Union's FP7 research and innovation and innovation programme under the Marie Sklodowska-Curie grant agreement No 291803."
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 IMDEA Software Institute participates in a new project funded by MINECO within the framework of RETOS-Colaboración 2016 call, coordinated by Scytl.
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 a new project funded by MINECO within the framework of RETOS-Colaboración 2016 call, coordinated by Scytl.
The goal of the project, entitled "AxE Javascript: Auditable E-voting using Javascript", is to bring a solution to confidence problems in the field of security in electronic voting systems through the development of an e-voting software with the highest possible correctness and security properties. Identifying and defining properties for security in e-voting systems and developing and implementing new methods providing real evidence of correctness and security in these systems. This will allow an important improvement in the transparency of e-voting systems used by electoral organizations. The project includes the participation of IMDEA Software researcher Gilles Barthe.
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) .
About Con ciencia en la escuela (in Spanish)
EIT Digital has today opened a node in Madrid to strengthen development of digital innovation in Spain. Tibor Navracsics, Commissioner for Education, Culture, Youth and Sport and Íñigo Méndez de Vigo, Spanish Minister for Education, Culture, and Sport, attended the opening at the IMDEA Software Institute and welcomed the closer integration of the Spanish innovation ecosystem into the European market through the new EIT Digital Node.
EIT Digital officially announced today that Madrid has become a full Node as of January 1, 2017. The Madrid Node now has the same rights as the eight other European Nodes of EIT Digital (Berlin, Eindhoven, Helsinki, London, Madrid, Paris, Stockholm and Trento), which offers great opportunities for Spain in driving forward digital transformation across Europe. EIT Digital has been present in Spain via its Madrid Associate Partner Group (APG) since 2013. Over four years from 2013-16, nearly €20 million was invested in Spain. Becoming a full Node enables a faster expansion of activities as is demonstrate by the fact that €15 million is being invested in 2017 alone in Spanish Innovation & Entrepreneurship as well as Entrepreuneurial Education activities.
Tibor Navracsics, Commissioner for Education, Culture, Youth and Sport, stated: "Innovation brings global benefits, but it begins with people at local or regional level. By establishing this Node in Madrid, EIT Digital is creating new opportunities in the region, providing space where researchers, entrepreneurs and educators can learn from each other and produce innovative new products and services - and educating the next generation of young thought leaders." Willem Jonker, CEO of EIT Digital, said: "I am very happy with the establishment of a full Node in Spain, which enables a significant increase of our innovation and entrepreneurial education activities in Spain."
EIT Digital's Spanish partners include Atos, the IMDEA Software Institute, Indra, Ferrovial, the Technical University of Madrid (UPM), Nokia-Spain and Telefonica.
IMDEA Software researcher Juan Caballero will be part of an effort to develop an online banking anti-fraud system. This work is supported by the EIT Digital’s 'Digital Finance' Action Line.
The “Online banking anti-fraud monitoring” innovation activity is one of three innovation activities of the Digital Finance Action Line of EIT Digital in 2017. Digital Finance, also known as “FinTech” focusses on the delivery of innovative financial products and services through digital technology, with the objective of making financial systems more reliable, more transparent and customer friendly improving thus the banking experience for the people in the society and the reducing the dependency of banks on central infrastructures.
Coowry a startup enabling easy micro payments whose offices are located in the IMDEA Software building was featured in the Spanish newspaper ABC.
IMDEA Software Institute researcher Carmela Troncoso has participated in the 2nd INTERPOL Workshop on Privacy Enhancing Technologies held on the 30th of January in Lyon, France. Carmela's talk, entitled “Privacy-preserving systems: Systematic reasoning for design and evaluation.” explained how to tackle the system engineering problem from a privacy point of view, describing means to reason about embedding strong privacy guarantees into ICT systems, and means to approach the evaluation of private information leakage in such scenarios.
IMDEA Software Institute researcher Dario Fiore has won with colleagues Michael Backes (DE), Manuel Barbosa (PT), and Raphael M. Reischuk (CH) the first edition of the CNIL/Inria prize on privacy protection for their publication entitled “ADSNARK: Nearly Practical and Privacy-Preserving Proofs on Authenticated Data.” This prize was jointly organized by the CNIL and Inria, two french government bodies.
IMDEA Software Institute researcher Boris Köpf will be lecturing at the Spring school on “Security & Correctness in the Internet of Things 2017” that is going to be held from May 8th to May 12th in Graz, Austria.
The five winners of the EIT Digital Summer School Competition on Privacy, Security and Trust for the best project have visited EIT Digital Madrid Node located at IMDEA Software Institute as part of their prize. During their visit they have met researchers from IMDEA Software, Carmela Troncoso and Dario Fiore, who explained to them the Institute's activities in the field of privacy and cybersecurity and gave feedback about the security aspects of the potential new product that the winners have developed during their summer school. In addition to the research-oriented meeting, they also met the local Business Accelerator team and visited the cybersecurity business unit of Telefonica.
IMDEA Software Institute faculty member Aleks Nanevski receives a prestigious ERC Consolidator Grant for the project "Mathador - Type and Proof Structures for Concurrent Software Verification".
Concurrent programs are notoriously difficult to write because of the complexity of interaction between their components. This complexity comes into the sharpest focus if one tries to develop a mathematical, computer-checkable, proof that a concurrent program produces the desired result. The required effort for developing such a proof today is overwhelming even for the simplest concurrent programs, because of the combinatorial explosion associated with the component interaction.
The goal of the Mathador project is to study, decompose, and simplify the structure of mathematical proofs of concurrent programs, to the point where they can be developed on a regular basis. Mastering these proofs will mean that we know how to describe the interaction between concurrent components in an intellectually manageable way. In turn, this will directly impact how we think about, write, and understand concurrent software.
More information: ERC Press Release, and List of ERC Consolidator Grant Awardees.
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).
Also, IMDEA Software Institute’s researchers Manuel Carro, José Francisco Morales and John Gallagher are among the 38 program committee members.
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.
The successful candidates will do research under the supervision of Juan Caballero or César Sánchez.
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.
Website: http://software.imdea.org/Conferences/ICLP2016/
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”.
The IMDEA Software Institute faculty member Carmela Troncoso, participates on the ZISC workshop organized by the "Zurich Information Security & Privacy Center" of ETH Zurich.
Carmela's talk, that can be found here, describes systematic ways to reason about privacy when engineering systems. The first part of the talk makes explicit which are the design strategies followed by privacy experts when engineering privacy-preserving systems, and shows how these design strategies require the use of Privacy Enhancing Technologies. The second part describes systematic approaches to develop such technologies in an optimal manner to support the implementation of privacy by design.
The IMDEA Software Institute faculty member Dario Fiore, coauthors two papers to appear at important Cryptographic conferences.
The first, together with Anca Nitulescu from ENS Paris, is accepted at the 14th Theory of Cryptography Conference (TCC 2016-B). This work, entitled “On the (In)security of SNARKs in the Presence of Oracles”, studies and sheds light on the security properties of efficient cryptographic proof systems. The work was partially done while A. Nitulescu was a research intern at IMDEA Software Institute.
The second, co-authored by IMDEA Software's PhD student Luca Nizzardo, together with Katerina Mitrokotsa and Elena Pagnin from Chalmers University, is accepted at the 22nd Annual International Conference on the Theory and Applications of Cryptology and Information Security (ASIACRYPT 2016). This work, entitled “Multi-Key Homomorphic Authenticators”, proposes new cryptographic mechanisms that allow for certifying the correctness of data and computations.
The IMDEA Software Institute will participate in a newly funded Horizon 2020 EU project called ElasTest: an elastic platform for testing complex distributed large software systems. The ElasTest project will develop infrastructure to help developers test and validate “software in the large”, while maintaining compatibility with current practices and tools. ElasTest will use a combination of instrumentation, test orchestration and test recommendation specifically crafted for improving the software reliability in the large software and in particular for cloud applications. The ElasTest consortium involves 11 companies, universities, and research centers from 6 European countries. The IMDEA Software Institute involvement focuses on runtime verification (Dr. César Sánchez) and security (Dr. Juan Caballero). The project will launch on January 2017 and will last for 3 years.
Four papers by IMDEA Software Institute researchers have been accepted for publication at the 23rd ACM Conference on Computer and Communications Security to be held in Vienna, Austria, at the end of October:
Dario Fiore's work, entitled "Hash First, Argue Later: Adaptive Verifiable Computations on Outsourced Data", is co-authored by Cédric Fournet, Markulf Kohlweiss, Olga Ohrimenko and Bryan Parno from Microsoft Research, and Esha Ghosh from Brown University. This paper proposes new cryptographic schemes that enforce third parties to perform computations correctly.
The other three papers are co-authored by IMDEA Software Institute faculty member Gilles Barthe and former faculty member Pierre-Yves Strub. The first paper, "Advanced Probabilistic Couplings for Differential Privacy", with Noémie Fong (ENS & IMDEA Software Institute), Marco Gaboardi (University at Buffalo, SUNY), Benjamin Grégoire (Inria), and Justin Hsu (University of Pennsylvania), provides new techniques to formally verify differentially private algorithms.
On the same vein, their second paper: "Differentially Private Bayesian Programming", with Gian Pietro Farina and Marco Gaboardi (University at Buffalo, SUNY), Emilio Jesús Gallego Arias (CRI Mines – ParisTech), Andrew D. Gordon (Microsoft Research), and Justin Hsu (University of Pennsylvania), presents novel means for writing and verifying differentially private Bayesian machine learning algorithms.
Finally, their third paper, "Strong non-interference and type-directed higher-order masking", with Sonia Belaïd (Thales Communications & Security), Pierre-Alain Fouque (Université Rennes 1), Benjamin Grégoire (Inria), Rebecca Zucchini (Inria), and François Dupressoir (former IMDEA Software Institute member), presents a fully automated methodology to verify the probing security of masked algorithms against differential power analysis, and generate masked versions from unprotected descriptions of an algorithm.
More information at CCS 2016.
IMDEA Software Institute’s researchers Manuel Hermenegildo and Pedro López-García, were the Program Committee chairs of the 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016) held in Edinburgh, Scotland UK, September 6-8, 2016, co-located with 18th International Symposium on Principles and Practice of Declarative Programming, PPDP, and the 23rd. Static Analysis Symposium, SAS. The program can be found here. The International Symposium on Logic-Based Program Synthesis and Transformation aims to stimulate and promote international research and collaboration in logic-based program development in any language paradigm.
IMDEA Software Institute faculty member Alexey Gotsman receives a prestigious ERC Starting Grant. His project is called RACCOON - A Rigorous Approach to Consistency in Cloud Databases.
More information: ERC Press Release, and List of ERC Starting Grant Awardees.
Spanish Media: Europa concede 28 millones de euros a 19 investigadores de España
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.
The Malicia Lab at the IMDEA Software Institute, led by Juan Caballero, has open-sourced AVClass, a tool for massive malware labeling.
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.
Notiweb, the science and technology news publishing service of madri+d, published an interview with researcher Juan Caballero on the “dark side” of software.
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.
More information can be found at the MSR-IMDEASW Joint Research Center web site and the Workshop site at Microsoft Research.
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 Bartheand 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.
Antonio Nappa was advised by IMDEA Software Institute faculty member Juan Caballero and obtained his degree from Universidad Politécnica de Madrid with a “cum laude” mention.
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:
Course info at EIT Digital | EIT Digital Madrid DTC | Madrid EIT DIGITAL APG | CAIT UPM | UPM | IMDEA Software Institute
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.
The NEXTLEAP kick-off meeting, was held in Paris, France, on February 15-16, 2016, and was attended by Carmela Troncoso, project leader of the project at the IMDEA Software Institute.
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.
IMDEA Software Institute researchers Juan Caballero and Jesús Contreras have been elected to serve as mentors on the first Spanish Cybersecurity Accelerator Program.
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:
The event page at EIT Digital.
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 ’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”.
Official announcement and more information.
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.
Alejandro Sánchez was advised by IMDEA Software Institute faculty member César Sánchez and obtained his degree from Universidad Politécnica de Madrid with a "cum laude" mention.
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 Fiorehas 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 Prabhakarand 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 , and coauthors Benjamin Beurdouche (INRIA), Karthikeyan Bhargavan (INRIA), Antoine Delignat-Lavaud (INRIA), Cedric Fournet (Microsoft Research), Markulf Kohlweiss (Microsoft Research), Alfredo Pironti (INRIA), and Jean Karim Zinzindohoue (INRIA), received the distinguished paper award at the 2015 IEEE Symposium on Security and Privacy (S&P ’15) for their research paper entitled “A Messy State of the Union: Taming the Composite State Machines of TLS”.
IMDEA Software Institute PhD student Antonio Nappa, along with researchers from the International Computer Science Institute in Berkeley CA and other researchers from Google Inc. received the distinguished practical paper award at the S&P ’15 for their practical contribution entitled “Ad Injection at Scale: Assessing Deceptive Advertisement Modifications”.
The official announcement is available here.
The first scientific meeting of the EU COST Action "Runtime Verification beyond Monitoring (ARVI)" has taken place in Valletta, Malta on April 9th and 10th. IMDEA Software Institute faculty member César Sánchez is a member of the management committee and a workgroup leader, and a leader in the COST Action proposal’s elaboration.
Runtime verification (RV) is a computing analysis paradigm based on observing a system at runtime to check its expected behavior. RV has emerged in recent years as a practical application of formal verification, and a less ad-hoc approach to conventional testing by building monitors from formal specifications.
The main goals of the action are:
to create an infrastructure that supports comparing tools and reusing existing infrastructure in runtime verification,
to explore potential impactful applications of runtime verification to industrial settings like hardware, medical devices, cloud computing, and even human centric systems, and
to explore challenging application domains for monitoring and runtime verification, such as hybrid systems and distributed systems.
Given the importance of computer-based industries in Europe, novel applications of RV have a large impact in terms of the new class of designs enabled and their reliability and cost effectiveness.
This COST Action is funded for 4 years, until 2018.
The thesis presents a novel, tool-supported model-driven methodology for developing secure data-management applications. With the methodology defined, developers proceed by modeling three different views of the desired application: its data model, security model, and GUI model. These models formalize respectively the application's data domain, authorization policy, and its graphical interface together with its behavior. Afterwards a model-transformation function automatically lifts the policy specified by the security model to the GUI model. Finally, a code generator automatically generates a multi-tier application, along with all support for access control, from the security-aware GUI model. Miguel Ángel García de Dios was advised by IMDEA Software Institute faculty member Manuel Clavel and obtained his degree from Universidad Complutense de Madrid.
Four papers by IMDEA Software Institute researchers have been accepted for publication in the proceedings of the 27th International Conference on Computer Aided Verification, a top-ranked conference in this important field, held this year in San Francisco, CA. These four papers are among 68 selected for publication from over 250 submissions.
IMDEA Software Institute faculty member César Sánchez has a paper on model checking “hyperproperties”, together with Bernd Finkbeiner and Markus Rabe from Saarland University, Germany. Their paper characterizes the precise complexity of the model checking problem for hyperproperties, and shows how to leverage existing state-of-the-art model checking tools to handle hyperproperty specifications, with applications to security, symmetry, and coding theory.
IMDEA Software Institute faculty member Boris Köpf has a paper together with Klaus von Gleissenthall ((TU Munich) and Andrey Rybalchenko (Microsoft Research) on verifying quantitative program properties, such as bounds on resource usage or information leaks. The core technical novelty is an SMT-based algorithm for synthesizing interpolants with cardinality constraints that relies on the theory of counting integer points in symbolic polytopes.
IMDEA Software Institute faculty member Michael Emmi’s contribution reports on the development of a tool for uncovering concurrency bugs in Android apps, a joint work with Burcu Kulahcioglu Ozkan and Serdar Tasiran of Koç University in Turkey.
IMDEA Software Institute faculty member Pierre Ganty has a paper on the automated verification of shared-memory asynchronous systems together with A. Durand-Gasselin, J. Esparza from TU Munich and R. Majumdar from Max Planck Institute for Software Systems, Saarbruecken, 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.
More information can be found at the MSR-IMDEASW Joint Research Center web site and the Workshop site at Microsoft Research.
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 , 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. 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 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:
They had the opportunity to discuss their ideas with IMDEA Software Institute faculty members Gilles Barthe, Juan Caballero, Dario Fiore, and Manuel Hermenegildo.
The visit was organized and moderated by Jesús Contreras, EIT Digital Business Developer at the Madrid CLC.
More info on the Summer Schools.
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:
More information can be found at the MSR-IMDEASW Joint Research Center web site and the Workshop site at Microsoft Research.
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.
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
Website: ENTRA
The IMDEA network of institutes has been granted AMAROUT-II, an EU Marie Curie (PEOPLE-COFUND) program that will offer 152 fellowships during the next 4 years to experienced researchers to help develop their individual research projects within any one of the research institutes comprising the IMDEA network. Each fellowship funds a researcher for up to three years. A permanent call for applications will be opened on October, 1 2012 and will run until September, 30 2015, with periodic closing dates. The program, prepared and coordinated by the IMDEA Software Institute, is designed to support transnational mobility of experienced researchers offering attractive working conditions and providing opportunities to deepen and widen their skills. AMAROUT-II is a continuation of AMAROUT, a highly successful COFUND program which is now closed for applications.
For more information see AMAROUT-II. Contact:
The IMDEA Software Institute has published its 2011 Annual Report.
Santiago Zanella, who completed his PhD at the IMDEA Software Institute under the supervision of Prof. Gilles Barthe, is the winner of the 2011 EAPLS Best Dissertation Award for his dissertation "Formal Certification of Game-Based Cryptographic Proofs" defended at the École Nationale Supérieure des Mines de Paris in 2010.
This award is given by the European Association on Programming Languages and Systems to the PhD student who has made the most original and influential contribution to the area of Programming Languages and Systems, and has graduated in the period up to November 2011 at a European academic institute. The purpose of the award is to draw attention to excellent work, to help the career of the student in question, and to promote the research field as a whole.
The winner was selected by a committee of international experts. Details on the procedure can be found here. The candidate theses were judged on originality, impact, relevance, and quality of writing.
With this award already two researchers associated with the IMDEA Software Institute have received this prestigious recognition.
IMDEA Software Institute researchers Alexey Gotsman and Mark Marron each got one of the 10 Microsoft Software Engineering Innovation Foundation (SEIF) Awards given by Microsoft Research in 2012.
Microsoft Research created these Awards to support research in software engineering technologies, tools, practices, and teaching methods. Out of more than 100 applications, only 8 other applicants, in addition to Alexey Gotsman and Mark Marron from the IMDEA Software Institute in Spain, obtained this prestigious award in 2011, 1 in Switzerland, 1 in Canada, and 6 in the United States.
Alexey Gotsman and Mark Marron will be publicly recognized at the new annual SEIF Day, to be held on 18th of July 2012, in Redmond, USA. This event is a new addition to the SEIF program and will be attended by previous and current SEIF winners, influential software engineering researchers, and researchers from Microsoft Research.
The paper Constraint-Based Runtime Prediction of SLA Violations in Service Orchestrations, co-authored by IMDEA Software Institute and UPM Researchers Dragan Ivanovic, Manuel Carro, and Manuel Hermenegildo, was selected as the Best Paper Award at ICSOC 2011, the 9th International Conference on Service Computing held at the Paphos, Cyprus, Dec 5–8, 2011.
The paper presents and evaluates a technique to detect ahead of time whether there will be or not SLA violations in service orchestrations, and to determine under which conditions these will (or will not) happen. The technique uses a model of the process which can evolve as the process executes, thus making it possible to reflect dynamic changes. At every inspection point, the continuation of the process model is sent to the predictor which produces a constraint model by means of symbolic execution using a constraint-generating interpreter. The constraint system is fed into a Prolog-based constraint solver which is, additionally, given boundary conditions to represent scenarios of failure and non-failure. The results of the constraint solver indicate the cases under which these scenarios will or may occur. Evaluations under realistic conditions obtained using the Microsoft Workflow Engine indicate significant prediction capacity with very small numbers of false positives / negatives.
The paper Computer-Aided Security Proofs for the Working Cryptographer, co-authored by IMDEA Software Institute Researchers Gilles Barthe and Santiago Zanella with colleagues at INRIA, is the winner of the Best Paper Award at CRYPTO 2011, the 31st International Cryptology Conference held at the University of California, Santa Barbara, Aug 14–18, 2011.
You can see the presentation at CRYPTO'11 here:
The paper presents EasyCrypt, an automated tool for elaborating security proofs of cryptographic systems which uses off-the-shelf SMT solvers and automated theorem provers. The tool is significantly easier to use than its predecessors and is arguably a plausible candidate for adoption by working cryptographers. The usefulness of the tool is illustrated through its application to security proofs of the Cramer-Shoup and Hashed ElGamal cryptosystems.
The paper Measuring Pay-per-Install: The Commoditization of Malware Distribution, co-authored by IMDEA Software Institute Assistant Professor Juan Caballero, is the winner of an Outstanding Paper Award at the Usenix Security 2011 Symposium.
The paper reports on recent research by Caballero and colleagues from the University of California, Berkeley, suggesting that most malware in personal computers is covertly installed by enterprising hackers, who sell access to the compromised hosts to criminal gangs in an underground Pay-Per-Install (PPI) market. The article was recently the subject of a feature in MIT's Technology review.
Manuel Hermenegildo, Institute Director, was, with Professors Michael Leuschel (University of Düsseldorf) and Antonio Porto (University of Lisbon) part of the winning team of the 18th Prolog Programming Contest at the 27th International Conference on Logic Programming in Lexington, Kentucky, USA. Of course, this was done using Ciao which was duly declared "this year's Prolog system of choice." And all of this while having to endure being continuously referred to by the contest organizers as the "old boys" team...
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.
Manuel Hermenegildo, Director of IMDEA Software, has been elected to the Academia Europaea.
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.
