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 research in the field of security and cryptography presented at a top conference

The research carried out by a team of researchers from INESC TEC’s High-assurance Software Laboratory (HASLab), in the field of computer security, led ​to the presentation of three scientific articles at the ​​ACM Conference on Computer and Communications Security (CCS)​​, one of the most important conferences in this area – which took place online between November 15 and 18.

19th November 2021

European project promotes cooperation across continents to improve high-performance computing

High Performance Computing (HPC) is the foundation for scientific, industrial and social advances that improve the quality of life for people worldwide. The main objective of the RISC2 project – A network for supporting the coordination of Computing research between Europe and Latin America – is to promote and improve the relationship between the research and industrial communities of Europe and Latin America, focusing on HPC applications and infrastructures’ implementation.

14th November 2021

INESC TEC will develop mathematical methods to advance cyber-physical programming

INESC TEC's High-Assurance Software Laboratory (HASLab) coordinates the project “Quantitative methods for cyber-physical programming: reasoning precisely about imprecisions in cyber-physical behavior”, whose main objective is the development of mathematical methods to model and analyse imprecisions in cyber-physical software.

08th September 2021

INESC TEC develops solutions to reduce the energy impact of communication networks

INESC TEC's High-Assurance Software Laboratory (HASLab) will develop solutions that allow the adaptation of WAN (Wide Area Networks) communications networks to the availability and source of electrical power in real time, while prioritising renewable sources.

06th September 2021

INESC TEC researchers awarded “Best Paper Award” in the field of Computing

The paper “ASPAS: As Secure as Possible Available Systems”, co-authored by Houssam Yactine, Ali Shoker, and George Younes, researchers at INESC TEC’s High-Assurance Software Laboratory (HASLab), received the Best Paper Award at the 16th edition of the International Federated Conference on Distributed Computing Techniques (DisCoTec2021).

15th July 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

2024

Trainability issues in quantum policy gradients

Authors
Sequeira, A; Santos, LP; Barbosa, LS;

Publication
MACHINE LEARNING-SCIENCE AND TECHNOLOGY

Abstract
This research explores the trainability of Parameterized Quantum Circuit-based policies in Reinforcement Learning, an area that has recently seen a surge in empirical exploration. While some studies suggest improved sample complexity using quantum gradient estimation, the efficient trainability of these policies remains an open question. Our findings reveal significant challenges, including standard Barren Plateaus with exponentially small gradients and gradient explosion. These phenomena depend on the type of basis-state partitioning and the mapping of these partitions onto actions. For a polynomial number of actions, a trainable window can be ensured with a polynomial number of measurements if a contiguous-like partitioning of basis-states is employed. These results are empirically validated in a multi-armed bandit environment.

2024

Trainability issues in quantum policy gradients with softmax activations

Authors
Sequeira, A; Santos, LP; Barbosa, LS;

Publication
2024 IEEE INTERNATIONAL CONFERENCE ON QUANTUM COMPUTING AND ENGINEERING, QCE, VOL 2

Abstract
This research addresses the trainability of Parameterized Quantum Circuit-based Softmax policies in Reinforcement Learning. We assess the trainability of these policies by examining the scaling of the expected value of the partial derivative of the log policy objective function. Here, we assume the hardware-efficient ansatz with blocks forming local 2-designs. In this setting, we show that if each expectation value representing the action's numerical preference is composed of a global observable, it leads to exponentially vanishing gradients. In contrast, for n-qubit systems, if the observables are log(n)-local, the gradients vanish polynomially with the number of qubits provided O(log n) depth. We also show that the expectation of the gradient of the log policy objective depend on the entire action space. Thus, even though global observables lead to concentration, the gradient signal can still be propagated in the presence of at least a single local observable. We validate the theoretical predictions in a series of ansatze and evaluate the performance of local and global observables in a multi-armed bandit setting.

2024

The Blocklace: A Universal, Byzantine Fault-Tolerant, Conflict-free Replicated Data Type

Authors
Almeida, PS; Shapiro, E;

Publication
CoRR

Abstract

2024

A Framework for Consistency Models in Distributed Systems

Authors
Almeida, PS;

Publication
CoRR

Abstract

2024

Validating multiple variants of an automotive light system with Alloy 6

Authors
Cunha, A; Macedo, N; Liu, C;

Publication
INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER

Abstract
This paper reports on the development and validation of a formal model for an automotive adaptive exterior lights system (ELS) with multiple variants in Alloy 6, which is the most recent version of the Alloy lightweight formal specification language that supports mutable relations and temporal logic. We explore different strategies to address variability, one in pure Alloy and another through an annotative language extension. We then show how Alloy and its Analyzer can be used to validate systems of this nature, namely by checking that the reference scenarios are admissible, and to automatically verify whether the established requirements hold. A prototype was developed to translate the provided validation sequences into Alloy and back to further automate the validation process. The resulting ELS model was validated against the provided validation sequences and verified for most of requirements for all variants.

Facts & Figures

68Researchers

2016

1R&D Employees

2020

16Academic Staff

2020

Contacts