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 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

Sustainable HPC: kick-off of the new project that aims to improve the sustainability of supercomputers’ operation

The Sustainable HPC project which, results from an (approved) application to the Innovation and Energy Efficiency Funds by INESC TEC and INEGI, has started.

25th November 2021

007

Projects

BringTrust

Strengthening CI/CD Pipeline Cybersecurity and Safeguarding the Intellectual Property

2025-2028

DisaggregatedHPC

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

2025-2026

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

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

2024

Performance and explainability of feature selection-boosted tree-based classifiers for COVID-19 detection

Authors
Rufino, J; Ramírez, JM; Aguilar, J; Baquero, C; Champati, J; Frey, D; Lillo, RE; Fernández Anta, A;

Publication
HELIYON

Abstract
In this paper, we evaluate the performance and analyze the explainability of machine learning models boosted by feature selection in predicting COVID-19-positive cases from self-reported information. In essence, this work describes a methodology to identify COVID-19 infections that considers the large amount of information collected by the University of Maryland Global COVID-19 Trends and Impact Survey (UMD-CTIS). More precisely, this methodology performs a feature selection stage based on the recursive feature elimination (RFE) method to reduce the number of input variables without compromising detection accuracy. A tree-based supervised machine learning model is then optimized with the selected features to detect COVID-19-active cases. In contrast to previous approaches that use a limited set of selected symptoms, the proposed approach builds the detection engine considering a broad range of features including self-reported symptoms, local community information, vaccination acceptance, and isolation measures, among others. To implement the methodology, three different supervised classifiers were used: random forests (RF), light gradient boosting (LGB), and extreme gradient boosting (XGB). Based on data collected from the UMD-CTIS, we evaluated the detection performance of the methodology for four countries (Brazil, Canada, Japan, and South Africa) and two periods (2020 and 2021). The proposed approach was assessed in terms of various quality metrics: F1-score, sensitivity, specificity, precision, receiver operating characteristic (ROC), and area under the ROC curve (AUC). This work also shows the normalized daily incidence curves obtained by the proposed approach for the four countries. Finally, we perform an explainability analysis using Shapley values and feature importance to determine the relevance of each feature and the corresponding contribution for each country and each country/year.

2024

Pondering the Ugly Underbelly, and Whether Images Are Real

Authors
Hill, RK; Baquero, C;

Publication
Commun. ACM

Abstract
[No abstract available]

Facts & Figures

68Researchers

2016

1R&D Employees

2020

16Academic Staff

2020

Contacts