Source author record

Ahmed Rezine

Ahmed Rezine appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record

Catalog footprint

What is connected

4works
5topics
4close collaborators

Actions

Connect this record

Log in to claim

Research graph

See the researcher in context

Open full explorer

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

4 published item(s)

preprint2016arXiv

Quantifying the Information Leak in Cache Attacks through Symbolic Execution

Cache timing attacks allow attackers to infer the properties of a secret execution by observing cache hits and misses. But how much information can actually leak through such attacks? For a given program, a cache model, and an input, our CHALICE framework leverages symbolic execution to compute the amount of information that can possibly leak through cache attacks. At the core of CHALICE is a novel approach to quantify information leak that can highlight critical cache side-channel leaks on arbitrary binary code. In our evaluation on real-world programs from OpenSSL and Linux GDK libraries, CHALICE effectively quantifies information leaks: For an AES-128 implementation on Linux, for instance, CHALICE finds that a cache attack can leak as much as 127 out of 128 bits of the encryption key.

preprint2013arXiv

Proceedings 14th International Workshop on Verification of Infinite-State Systems

This volume contains the proceedings of Infinity'12, the 14th International Workshop on Verification of Infinite-State Systems, which was held in Paris, France on the 27th of August 2012 as a satellite event of FM'12. The aim of the INFINITY workshop is to provide a forum for researchers interested in the development of formal methods and algorithmic techniques for the analysis of systems with infinitely many states, and their application in automated verification of complex software and hardware systems.

preprint2012arXiv

Ordered Counter-Abstraction

We introduce a new symbolic representation based on an original generalization of counter abstraction. Unlike classical counter abstraction (used in the analysis of parameterized systems with unordered or unstructured topologies) the new representation is tailored for proving properties of linearly ordered parameterized systems, i.e., systems with arbitrary many finite processes placed in an array. The relative positions in the array capture the relative priorities of the processes. Configurations of such systems are finite words of arbitrary lengths. The processes communicate using global transitions constrained by their relative priorities. Intuitively, an element of the symbolic representation has a base and a set of counters. It denotes configurations that respect the constraints imposed by the counters and that have the base as a sub word. We use the new representation in a uniform and automatic Counter Example Guided Refinement scheme. We introduce a relaxation operator that allows a well quasi ordering argument for the termination of each iteration of the refinement loop. We explain how to refine the relaxation to systematically prune out false positives. We implemented a tool to illustrate the approach on a number of parameterized systems.