Abstract

Abstract
Secure multiparty computation (SMC) allows for complex computations over encrypted data. Privacy concerns for cloud applications makes this a highly desired technology and recent performance improvements show that it is practical. To make SMC accessible to non-experts and empower its use in varied applications, many domain-specific compilers are being proposed.We review the role of these compilers and provide a formal treatment of the core steps that they perform to bridge the abstraction gap between high-level ideal specifications and efficient SMC protocols. Our abstract framework bridges this secure compilation problem across two dimensions: 1) language-based source- to target-level semantic and efficiency gaps, and 2) cryptographic ideal- to real-world security gaps. We link the former to the setting of certified compilation, paving the way to leverage long-run efforts such as CompCert in future SMC compilers. Security is framed in the standard cryptographic sense. Our results are supported by a machine-checked formalisation carried out in EasyCrypt.

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

Abstract
The paper presents the work carried out at the HCI Engineering Education workshop, organised by IFIP working groups 2.7/13.4 and 13.1. It describes four case studies of projects and exercises used in Human-Computer Interaction Engineering courses. We propose a common framework for presenting the case studies and describe the four case studies in detail. We then draw conclusions on the differences between the presented case studies that highlight the diversity and multidisciplinary aspects to be taught in a Human-Computer Interaction Engineering course. As future work, we plan to create a repository of case studies as a resource for teachers.

Abstract
This paper arises from experience by the authors in teaching software engineering courses. It discusses the need for adequate coverage of Human-Computer Interaction topics in these courses and the challenges faced when addressing them. Three courses, at both licentiate and master's levels, are used as triggers for the discussion. The paper argues that the lack of relevant Human-Computer Interaction concepts creates challenges when teaching and learning requirements analysis, design, and implementation of software systems. The approaches adopted to address these challenges are described.