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