While users tend to indiscriminately use the same device to address every need, exfiltration of information becomes the end game of attackers. Average users need realistic and practical solutions to enable them to mitigate the consequences of a security breach in terms of data leakage. We present StemJail, an open-source security solution to isolate groups of processes pertaining to the same activity into an environment exposing only the relevant subset of user data. At the heart of our solution lies dynamic activity discovery, allowing seamless integration of StemJail into the user workflow. Our userland access control framework only relies on the ability of user to organize data in directories. Thus, it is easily configurable and requires very little user interaction once set up. Moreover, StemJail is designed to run without intrusive changes to the system and to be configured and used by any unprivileged user thanks to the Linux user namespaces.

Hash functions are the swiss army knife of cryptographers. They are used to generate unique identifiers in hash-and-sign signatures, as one-way functions for one-time-password, to break the structure of the input in key derivation functions and also for authentications. We propose a formal analysis of domain extenders for hash functions in the in differentiability framework. We define a general model for domain extenders and provide a unified proof of their security in the form of a generic reduction theorem. Our general model captures many iterated constructions such as domain extenders, modes of operation of symmetric cryptography such as CBC-MAC or block ciphers based on Feistel networks. Its proof has been carried out using the Computational Indistinguishability Logic of Barthe et al.. The theorem can help designers of hash functions justifying the security of their constructions: they only need to bound the probability of well-defined events. Our model allows to consider many SHA-3 finalists and is instantiated on two well-known constructions, namely Chop-MD and Sponge. Finally, the in differentiability bounds which we prove are convincing since they match previous proofs and the application of our result on the sponge construction (underlying the Keccak design) highlights the lack of an additional term in the bound provided by Bertoni et al., as was anticipated but not justified by Bresson et al..

Computational Indistinguishability Logic (CIL) is a logic for reasoning about cryptographic primitives in computational models. It captures reasoning patterns that are common in provable security, such as simulations and reductions. CIL is sound for the standard model, but also supports reasoning in the random oracle and other idealized models.

Chosen-ciphertext security is by now a standard security property for asymmetric encryption. Many generic constructions for building secure cryptosystems from primitives with lower level of security have been proposed. Providing security proofs has also become standard practice. There is, however, a lack of automated verification procedures that analyze such cryptosystems and provide security proofs. This paper presents an automated procedure for analyzing generic asymmetric encryption schemes in the random oracle model. It has been applied to several examples of encryption schemes among which the construction of Bellare-Rogaway 1993, of Pointcheval at PKC'2000 and REACT.