ABSTRACT. Password managers (PMs) are important tools that enable the use of stronger passwords, freeing users from the cognitive burden of remembering them. Despite this, there are still many users who do not fully trust PMs. In this paper, we focus on a feature that most PMs offer that might impact the user's trust, which is the process of generating a random password. We present three of the most commonly used algorithms and we propose a solution for a formally verified reference implementation of a password generation algorithm. We use EasyCrypt to specify and verify our reference implementation. In addition, we present a proof-of-concept prototype that extends Bitwarden to only generate compliant passwords, solving a frequent users' frustration with PMs. This demonstrates that our formally verified component can be integrated into an existing (and widely used) PM.

ABSTRACT. From the very outset of the digital era, the protection of personal data against unauthorized usage and distribution has been one of the most significant challenges in distributed services. For this reason, new regulations such as the European Union's General Data Protection Regulation grant users exceptional control over their data that is handled by businesses. Compliance with such regulations can take expensive refitting of the existing systems and manual work. We propose a formal language that can define properties like informed consent, data subject rights, and the lawfulness of the processing with programming language constructs to capture data protection requirements. The language is designed to abstract ownership information to make data dependencies explicit. We formalise a notion of policy compliance. This can be useful in service architecture with various actors who necessarily do not trust each other and may have conflicting interests.

ABSTRACT. This paper presents a new data flow coverage criterion for a deeper analysis of possible refinements to the constraints on paths unfolding of software program’s behavior. Such refinements represent a feasible chain of usages of the same variable without redefinitions in-between. Algorithm for reasonable chains selection is proposed.

ABSTRACT. Static analyses based on typestates are important in certifying correctness of code contracts. Such analyses rely on Deterministic Finite Automata (DFAs) to specify properties of an object. We target the analysis of contracts in low-latency environments, where many useful contracts are impractical to codify as DFAs and/or the size of their associated DFAs leads to sub-par performance. To address this bottleneck, we present a lightweight typestate analyzer, based on an expressive specification language that can succinctly specify code contracts. By implementing it in the static analyzer Infer, we demonstrate considerable performance and usability benefits when compared to existing techniques. A central insight is to rely on a sub-class of DFAs with efficient bit-vector operations.