IMDEA initiative
Abstract: Some weeks ago I found an interesting bug in Chrome and spent the weekend trying to come up with a clever exploit. In th...
Abstract: In this talk I will show you how to use standard playing cards in order to run cryptographic protocols in a visual and e...
Abstract: Software verification comes in two flavors: static and dynamic. Static program verification takes place during program a...
Abstract: For type checking of functional programming languages, it is fundamental to be able to check equality of types, or in ot...
Abstract: Attribute-based credentials are a privacy-enhancing technology that allow users to prove things about themselves in a pr...
Abstract: s(ASP) is a system which computes stable models of logic programs extended with negation (i.e., a logic program with no ...
Abstract: The Split State Model allows to obtain tamper and leakage resilience against a big class of attackers. In this model the...
Abstract: Attribute-based encryption (ABE) is a cryptographic primitive which supports fine-grained access control on encrypted da...
Abstract: Procedure specifications are useful in many software development tasks. As one example, in automatic test case generatio...
Abstract: Malware lineage studies the evolutionary relationships among malware and has important applications for malware analysis...
Abstract: Motivated by applications to security and high efficiency, we propose an automated methodology for validating on low-lev...
Abstract: Context-sensitive global analysis of large code bases can be expensive, which can be specially problematic in interactiv...
Abstract: Potentially unwanted programs (PUP) are a category of undesirable software which includes adware and rogueware. PUP is o...
Abstract: Proofs of computational effort were devised to control denial of service attacks. Dwork and Naor (CRYPTO ‘92), for...
Abstract: The Paxos algorithm of Lamport is a classic consensus protocol for state machine replication in environments that admit ...
Abstract: Untyped languages offer great flexibility in term creation and manipulation. To ensure correctness of data operations ex...
Abstract: We present a preliminary study to understand how apps evolve in their permission requests across different releases. We ...
Abstract: Relational program verification is a variant of program verification where one can reason about two programs and as a sp...
Abstract: Along with the conventional mathematic-driven approach of software security, 20 years of attacks harnessing the timing b...
Abstract: There exist two main formalisms to describe context-free languages: context-free grammars and pushdown automata. In fact...
Abstract: Arguments about correctness of a concurrent data structure are typically carried out by using the notion of linearizabil...
Abstract: A promising approach to defend against side channel attacks is to build programs that are leakage resilient, in a formal...
Abstract: In the last years we have witnessed a boom in the use of techniques and tools that provide anonymity. Such techniques an...
Abstract: Input validation is the first line of defense against malformed or malicious inputs. It is therefore critical that the v...
Abstract: The interest in reasoning over stream data is growing as quickly as the amount of data generated. Our intention is to ch...
Abstract: Homomorphic authenticators (HAs) enable a client to authenticate a large collection of data elements m_1, … , m_t...
