Cookies Policy
The website need some cookies and similar means to function. If you permit us, we will use those means to collect data on your visits for aggregated statistics to improve our service. Find out More
Accept Reject
  • Menu
Facts & Numbers
000
Presentation

High-Assurance Software

HASLab is focused on the design and implementation of high-assurance software systems: software that is correct by design and resilient to environment faults and malicious attacks. 

To accomplish this mission, HASLab covers three main competences — Cybersecurity, Distributed Systems, and Software Engineering — complemented by other competences such as Human-Computer Interaction, Programming Languages, or the Mathematics of Computing. 

Software Engineering – methods, techniques, and tools for rigorous software development, that can be applied to the internal functionality of a component, its composition with other components, as well as the interaction with the user.

Distributed Systems – improving the reliability and scalability of software, by exploring properties inherent to the distribution and replication of computer systems.

Cybersecurity – minimize the vulnerability of software components to hostile attacks, by deploying structures and cryptographic protocols whose security properties are formally proven.

Through a multidisciplinary approach that is based on solid theoretical foundations, we aim to provide solutions — theory, methods, languages, tools — for the development of complete ICT systems that provide strong guarantees to their owners and users. Prominent application areas of HASLab research include the development of safety and security critical software systems, the operation of secure cloud infrastructures, and the privacy-preserving management and processing of big data.

Latest News

INESC TEC team contributed to a new version of Alloy modelling language

Alcino Cunha and Nuno Macedo, INESC TEC researchers, contributed to the development of Alloy 6, the latest version of one of the most used specification and analysis platforms for the formal analysis of designs in the early stages of software development.  

11th May 2022

INESC TEC researchers acknowledged at international conference on software engineering

The paper “Schema-guided  Testing of Message-oriented Systems“, by Alcino Cunha and Nuno Macedo, researchers at INESC TEC, and André Santos, engineer at CoLAB VORTEX, was the winner of the Best Paper Award at the 17th edition of the international conference ENASE – Conference on Evaluation of Novel Approaches to Software Engineering.

05th May 2022

INESC TEC research enables faster scientific studies performed on supercomputers

The work developed by INESC TEC researchers João Paulo and Ricardo Macedo aims at ensuring that scientists who use supercomputers can carry out scientific studies in fields like medicine, natural sciences, climate change and others, faster and more accurately. The results of the research work were presented in late February, at one of the most important conferences in storage systems: USENIX FAST.

11th March 2022

New tool reduces the cost of robots and increases their reliability and safety

Whether to clean our homes, manufacture products or even disable bombs, robotics is increasingly used, as it performs tasks faster and more efficiently. Focusing on the development of safer high-quality robotic applications, with lower costs, the Institute for Systems and Computer Engineering, Technology and Science (INESC TEC) created the HAROS tool within the scope of the SAFER project – Safety verification for robotic software.

09th February 2022

INESC TEC part of project to improve the development of high-assurance software

INESC TEC’s High-Assurance Software Laboratory (HASLab) coordinates the SpecRep (Constraint-based Specification Repair) project – which focuses on promoting the adequate formal specification of software components, crucial to the development of high-assurance software.

24th January 2022

011

Projects

ADAPQO

Adaptive Query Optimization Architectures to Support Heterogeneous Data Intensive Applications

2025-2026

BringTrust

Strengthening CI/CD Pipeline Cybersecurity and Safeguarding the Intellectual Property

2025-2028

SafeIaC

SafeIaC: Reliable Analysis and Automated Repair for Infrastructure as Code

2025-2028

ATAI

Aplicação de técnicas avançadas na gestão de escalas

2025-2027

DisaggregatedHPC

Towards energy-efficient, software-managed resource disaggregation in HPC infrastructures

2025-2026

PFAI4_6eD

Programa de Formação Avançada Industria 4 - 6a edição

2025-2025

InfraGov

InfraGov: A Public Framework for Reliable and Secure IT Infrastructure

2025-2026

VeriFixer

VeriFixer: Automated Repair for Verification-Aware Programming Languages

2025-2026

ENSCOMP4

Ensino de Ciência da Computação nas Escolas 4

2024-2025

PFAI4_5eD

Programa de Formação Avançada Industria 4 - 5a edição

2024-2024

QuantELM

QuantELM: from Ultrafast optical processors to Quantum Extreme Learning Machines with integrated optics

2023-2024

Team
001

Laboratory

CLOUDinha

Publications

HASLab Publications

View all Publications

2025

C'est Tres CHIC: A Compact Password-Authenticated Key Exchange from Lattice-Based KEM

Authors
Arriaga, A; Barbosa, M; Jarecki, S; Skrobot, M;

Publication
ADVANCES IN CRYPTOLOGY - ASIACRYPT 2024, PT V

Abstract
Driven by the NIST's post-quantum standardization efforts and the selection of Kyber as a lattice-based Key-Encapsulation Mechanism (KEM), severalPasswordAuthenticated KeyExchange (PAKE) protocols have been recently proposed that leverage a KEM to create an efficient, easy-to-implement and secure PAKE. In two recent works, Beguinet et al. (ACNS 2023) and Pan and Zeng (ASIACRYPT 2023) proposed generic compilers that transform KEM into PAKE, relying on an Ideal Cipher (IC) defined over a group. However, although IC on a group is often used in cryptographic protocols, special care must be taken to instantiate such objects in practice, especially when a low-entropy key is used. To address this concern, Dos Santos et al. (EUROCRYPT 2023) proposed a relaxation of the ICmodel under the Universal Composability (UC) framework called Half-Ideal Cipher (HIC). They demonstrate how to construct a UC-secure PAKE protocol, EKE-KEM, from a KEM and a modified 2round Feistel construction called m2F. Remarkably, the m2F sidesteps the use of an IC over a group, and instead employs an IC defined over a fixed-length bitstring domain, which is easier to instantiate. In this paper, we introduce a novel PAKE protocol called CHIC that improves the communication and computation efficiency of EKE-KEM, by avoiding the HIC abstraction. Instead, we split the KEM public key in two parts and use the m2F directly, without further randomization. We provide a detailed proof of the security of CHIC and establish precise security requirements for the underlying KEM, including one-wayness and anonymity of ciphertexts, and uniformity of public keys. Our findings extend to general KEM-based EKE-style protocols and show that a passively secure KEM is not sufficient. In this respect, our results align with those of Pan and Zeng (ASIACRYPT 2023), but contradict the analyses of KEM-to-PAKE compilers by Beguinet et al. (ACNS 2023) and Dos Santos et al. (EUROCRYPT 2023). Finally, we provide an implementation of CHIC, highlighting its minimal overhead compared to the underlying KEM - Kyber. An interesting aspect of the implementation is that we reuse the rejection sampling procedure in Kyber reference code to address the challenge of hashing onto the public key space. As of now, to the best of our knowledge, CHIC stands as the most efficient PAKE protocol from black-box KEM that offers rigorously proven UC security.

2025

A Tight Security Proof for SPHINCS+, Formally Verified

Authors
Barbosa, M; Dupressoir, F; Hülsing, A; Meijers, M; Strub, PY;

Publication
ADVANCES IN CRYPTOLOGY - ASIACRYPT 2024, PT IV

Abstract
SPHINCS+ is a post-quantum signature scheme that, at the time of writing, is being standardized as SLH-DSA. It is the most conservative option for post-quantum signatures, but the original tight proofs of security were flawed- as reported by Kudinov, Kiktenko and Fedorov in 2020. In this work, we formally prove a tight security bound for SPHINCS+ using the EasyCrypt proof assistant, establishing greater confidence in the general security of the scheme and that of the parameter sets considered for standardization. To this end, we reconstruct the tight security proof presented by Hulsing and Kudinov (in 2022) in a modular way. A small but important part of this effort involves a complex argument relating four different games at once, of a form not yet formalized in EasyCrypt (to the best of our knowledge). We describe our approach to overcoming this major challenge, and develop a general formal verification technique aimed at this type of reasoning. Enhancing the set of reusable EasyCrypt artifacts previously produced in the formal verification of stateful hash-based cryptographic constructions, we (1) improve and extend the existing libraries for hash functions and (2) develop new libraries for fundamental concepts related to hash-based cryptographic constructions, including Merkle trees. These enhancements, along with the formal verification technique we develop, further ease future formal verification endeavors in EasyCrypt, especially those concerning hash-based cryptographic constructions.

2025

Revisiting the Security and Privacy of FIDO2

Authors
Barbosa, M; Boldyreva, A; Chen, S; Cheng, K; Esquível, L;

Publication
IACR Cryptol. ePrint Arch.

Abstract

2025

NoIC: PAKE from KEM without Ideal Ciphers

Authors
Arriaga, A; Barbosa, M; Jarecki, S;

Publication
IACR Cryptol. ePrint Arch.

Abstract

2024

Exploring Frama-C Resources by Verifying Space Software

Authors
Busquim e Silva, RA; Arai, NN; Burgareli, LA; Parente de Oliveira, JM; Sousa Pinto, J;

Publication
Computer Science Foundations and Applied Logic

Abstract

Facts & Figures

0Book Chapters

2020

4Papers in indexed journals

2020

1R&D Employees

2020

Contacts