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
Computer Science and Engineering

Advanced computing as a bridge between Portugal and Japan: INESC TEC and AIST reinforce scientific cooperation

Five years have passed since INESC TEC and the National Institute of Advanced Industrial Science and Technology (AIST), in Japan, signed the first Memorandum of Understanding (MoU). This scientific cooperation agreement, focused on advanced computing, led to major opportunities for mobility, joint publications and the exchange of knowledge and experiences, thus bringing the Portuguese and Japanese R&D ecosystems closer together – particularly in High-Performance Computing (HPC). Recently, the two institutes renewed the MoU and will continue to work together to boost research in advanced computing.

03rd February 2025

Computer Science and Engineering

There are bridges uniting biomedical engineering and supercomputing - INESC TEC researchers flew to Barcelona to cross them

For a week, Alicia Oliveira and Beatriz Cepa left INESC TEC's laboratories in Braga and went to Barcelona - the city that welcomed the ACM Summer School. The researchers explored some of the elemental HPC concepts and realised that - in a context dominated by computer science - their training in biomedical engineering was an asset.

31st October 2024

Computer Science and Engineering

Software bugs are as persistent as those in nature - a study by INESC TEC closed in on them

INESC TEC researchers developed the LazyFS tool, capable of injecting faults and reproducing data loss bugs. The solution helps to understand the origin and cause of said bugs, but also to validate protection mechanisms against failures. 

07th October 2024

In the era of pervading data storage, replication can be the key to large-scale systems. Here’s how a INESC TEC research explores these challenges

In a study published in ACM Computing Surveys, Paulo Sérgio Almeida, INESC TEC researcher, synthesises the existing knowledge on approaches to Conflict-free Replicated Data Types, a topic he has been exploring over the past decade. These enable replication in distributed systems with automatic conflict resolution, ensuring high availability – even in the face of communication failures.

04th October 2024

INESC TEC with five FCT exploratory projects approved in four R&D areas

Telecommunications and Multimedia, Applied Photonics, High-assurance Software and Advanced Computing Systems – these are the four domains that INESC TEC researchers will explore within the scope of the five projects that were approved through the Call for Exploratory Projects promoted by the Foundation for Science and Technology (FCT).

02nd October 2024

013

Projects

ADAPQO

Adaptive Query Optimization Architectures to Support Heterogeneous Data Intensive Applications

2025-2026

JasminCode

Developing Reliable High-performance Assembly Code using Jasmin

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

BolsasFCT_Gestao

Funding FCT PhD Grants - Management

2025-9999

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

Understanding the adoption of modern Javascript features: An empirical study on open-source systems

Authors
Lucas, W; Nunes, R; Bonifácio, R; Carvalho, F; Lima, R; Silva, M; Torres, A; Accioly, P; Monteiro, E; Saraiva, J;

Publication
EMPIRICAL SOFTWARE ENGINEERING

Abstract
JavaScript is a widely used programming language initially designed to make the Web more dynamic in the 1990s. In the last decade, though, its scope has extended far beyond the Web, finding utility in backend development, desktop applications, and even IoT devices. To circumvent the needs of modern programming, JavaScript has undergone a remarkable evolution since its inception, with the groundbreaking release of its sixth version in 2015 (ECMAScript 6 standard). While adopting modern JavaScript features promises several benefits (such as improved code comprehension and maintenance), little is known about which modern features of the language have been used in practice (or even ignored by the community). To fill this gap, in this paper, we report the results of an empirical study that aims to understand the adoption trends of modern JavaScript features, and whether or not developers conduct rejuvenation efforts to replace legacy JavaScript constructs and idioms with modern ones in legacy systems. To this end, we mined the source code history of 158 JavaScript open-source projects, identified contributions to rejuvenate legacy code, and used time series to characterize the adoption trends of modern JavaScript features. The results of our study reveal extensive use of JavaScript modern features which are present in more than 80% of the analyzed projects. Our findings also reveal that (a) the widespread adoption of modern features happened between one and two years after the release of ES6 and, (b) a consistent trend toward increasing the adoption of modern JavaScript language features in open-source projects and (c) large efforts to rejuvenate the source code of their programs.

2025

Leakage-Free Probabilistic Jasmin Programs

Authors
Almeida, JB; Firsov, D; Oliveira, T; Unruh, D;

Publication
PROCEEDINGS OF THE 14TH ACM SIGPLAN INTERNATIONAL CONFERENCE ON CERTIFIED PROGRAMS AND PROOFS, CPP 2025

Abstract
This paper presents a semantic characterization of leakage-freeness through timing side-channels for Jasmin programs. Our characterization covers probabilistic Jasmin programs that are not constant-time. In addition, we provide a characterization in terms of probabilistic relational Hoare logic and prove the equivalence between both definitions. We also prove that our new characterizations are compositional and relate our new definitions to existing ones from prior work, which could only be applied to deterministic programs. To provide practical evidence, we use the Jasmin framework to develop a rejection sampling algorithm and provide an EasyCrypt proof that ensures the algorithm's implementation is leakage-free while not being constant-time.

2025

Formal Approaches for Interactive Systems

Authors
Campos, JC; Harrison, MD;

Publication
Handbook of Human Computer Interaction

Abstract

2025

Logic and Calculi for All on the occasion of Luis Barbosa's 60th birthday

Authors
Madeira, A; Oliveira, JN; Proença, J; Neves, R;

Publication
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING

Abstract
[No abstract available]

2025

Introduction to the Special Collection from FACS 2022

Authors
Tarifa, SLT; Proenca, J; Oliveira, J;

Publication
FORMAL ASPECTS OF COMPUTING

Abstract

Facts & Figures

0Book Chapters

2020

16Academic Staff

2020

21Senior Researchers

2016

Contacts