Cookies
O website necessita de alguns cookies e outros recursos semelhantes para funcionar. Caso o permita, o INESC TEC irá utilizar cookies para recolher dados sobre as suas visitas, contribuindo, assim, para estatísticas agregadas que permitem melhorar o nosso serviço. Ver mais
Aceitar Rejeitar
  • Menu
Factos & Números
000
Apresentação

Laboratório de Software Confiável

O HASLab dedica-se à criação e à implementação de sistemas de software confiável, i.e., software correto e resiliente perante falhas e ataques.

De forma a cumprir este grande objetivo, o HASLab opera em três grandes áreas - Cibersegurança, Sistemas Distribuídos e Engenharia de Software.

Engenharia de Software - são explorados métodos, técnicas e ferramentas para o desenvolvimento de software, podendo este ser integrado nas funcionalidades internas de determinados componentes, na sua configuração junto de outros componentes, e também na interação com o utilizador.

Sistemas Distribuídos - com vista a melhorar a confiabilidade e a escalabilidade de software, explorando as propriedades inerentes à distribuição e à replicação de sistemas computacionais.

Cibersegurança - de forma a minimizar a vulnerabilidade dos componentes de software a ataques, com recurso à implementação de estruturas e de protocolos criptográficos com propriedades de segurança formalmente comprovadas.

Através de uma abordagem multidisciplinar que assenta em princípios teóricos comprovados, o HASLab visa disponibilizar soluções - fundamentos teóricos, métodos, linguagens, ferramentas - para o desenvolvimento de sistemas TIC abrangentes, dando garantias aos seus proprietários e utilizadores. Os grandes domínios de aplicação da investigação desenvolvida no HASLab incluem o desenvolvimento de sistemas de software cruciais para garantir a segurança e a proteção, a operacionalização de infraestruturas da nuvem seguras, e a gestão e o tratamento de big data, tendo em conta as questões da privacidade.

Últimas Notícias
Ciência e Engenharia dos Computadores

Os bugs de software são tão persistentes como os da Natureza — uma investigação INESC TEC apertou-lhes a rede

Investigadores INESC TEC desenvolveram a ferramenta LazyFS, capaz de injetar faltas e reproduzir bugs de perda de dados. A solução vem ajudar a compreender a origem e a causa destes bugs, mas também validar mecanismos de proteção contra as falhas. 

07 outubro 2024

Na era do armazenamento incessante de dados, replicá-los pode ser a chave para sistemas de grande escala. Uma investigação INESC TEC explora esses desafios

Numa investigação publicada na revista ACM Computing Surveys, Paulo Sérgio Almeida, investigador do INESC TEC, sintetiza o conhecimento existente sobre abordagens aos Conflict-free Replicated Data Types, tópico que tem vindo a explorar na última década. Estes permitem replicação em sistemas distribuídos com resolução automática de conflitos, oferecendo grande disponibilidade — mesmo perante falhas de comunicação.

04 outubro 2024

INESC TEC com 5 projetos exploratórios FCT aprovados em 4 áreas de I&D

Telecomunicações e multimédia, fotónica aplicada, software confiável e sistemas de computação avançada – são estas as quatro áreas que os investigadores do INESC TEC vão trabalhar no âmbito dos cinco projetos que foram aprovados através do Concurso de Projetos Exploratórios da Fundação para a Ciência e a Tecnologia (FCT).

02 outubro 2024

Ciência e Engenharia dos Computadores

Há vantagens nas bases de dados edge — e os investigadores do INESC TEC dedicaram-se a estudá-las

O artigo Databases in Edge and Fog Environments: A Survey, assinado por Luís Manuel Ferreira, Fábio Coelho e José Orlando Pereira e publicado na ACM Computing Surveys, estabelece conceitos inovadores na área de base de dados edge, recorrendo a diversas publicações ao nível de hardware utilizado, performance de latência, consumo de energia e privacidade. Este novo tipo de bases de dados tira partido de dispositivos situados próximos do utilizador para melhorar o desempenho e as funcionalidades oferecidas pelas mesmas.

03 julho 2024

Ciência e Engenharia dos Computadores

Protótipo para apoiar o desenvolvimento de políticas e estratégias de defesa vale prémio a investigadora do INESC TEC

Alexandra Mendes, investigadora do INESC TEC, é uma das vencedoras do Atlantic Security Award, promovido pela FLAD, com uma proposta que visa a utilização de um grande modelo de linguagem (LLM – Large Language Model), treinado com dados da dark web, na tomada de decisão e na elaboração de políticas e estratégias de defesa, assim como na aplicação da lei na segurança da região do Atlântico.

28 maio 2024

059

Projetos Selecionados

INSIEME

Integrated Network for data Space and Interoperable Energy Management in Europe

2025-2028

JRCSIF

JRC Interoperability Laboratory Adoption of the Semantic Interoperability Framework

2025-2025

CDMS

Claim Denial Management Solution

2025-2026

PeT

PeT - Privacidade e Transparência

2024-2028

exaSIMPLE

exaSIMPLE: A Hybrid ML-CFD SIMPLE Algorithm for the Exascale Era

2024-2025

EPICURE

High-level specialised application support service in High-Performance Computing (HPC)

2024-2028

BCDSM

BCD.S+M - Sistema Modular de Armazenamento e Gestão de Dados em Blockchain com IA

2024-2027

TwinEU

Digital Twin for Europe

2024-2026

HEDGE_IoT

Holistic Approach towards Empowerment of the DiGitalization of the Energy Ecosystem through adoption of IoT solutions

2024-2027

HANAMI

Hpc AlliaNce for Applications and supercoMputing Innovation: the Europe - Japan collaboration

2024-2026

PFAI4_4eD

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

2023-2023

ATE

Aliança para a Transição Energética

2023-2026

Green_Dat_AI

Energy-efficient AI-ready Data Spaces

2023-2025

EuroCC2

National Competence Centres in the framework of EuroHPC Phase 2

2023-2025

AURORA

Deteção de atividade no interior do veículo

2022-2023

ATTRACT_DIH

Digital Innovation Hub for Artificial Intelligence and High-Performance Computing

2022-2025

NewSpacePortugal

Agenda New Space Portugal

2022-2025

BeFlexible

Boosting engagement to increase flexibility

2022-2026

ENERSHARE

European commoN EneRgy dataSpace framework enabling data sHaring-driven Across- and beyond- eneRgy sErvices

2022-2025

Gridsoft

Parecer sobre a implementação de software para redes elétricas inteligentes

2022-2022

PFAI4_3ed

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

2022-2022

THEIA

Automated Perception Driving

2022-2023

IBEX

Métodos quantitativos para a programação ciber-física: Uma abordagem precisa para racicionar sobre imprecisões na computação ciber-física

2022-2025

SpecRep

Constraint-based Specification Repair

2022-2023

FLEXCOMM

Towards Energy-aware Communications: Connecting the power grid and communication infrastructure

2022-2023

Sustainable HPC

Computação de elevado desempenho sustentável

2021-2025

CircThread

Building the Digital Thread for Circular Economy Product, Resource & Service Management

2021-2025

PassCert

Investigação do Impacto de Verificação Formal na Adopção de Software para Segurança de Passwords

2021-2022

IoT4Distribuicao

Análise de Requisitos e Especificação Funcional de uma Arquitetura Distribuída baseada em soluções IoT para a Gestão e Controlo da Rede de Distribuição

2021-2023

RISC2

A network for supporting the coordination of High-Performance Computing research between Europe and Latin America

2021-2023

PFAI4.0

Programa de Formação Avançada Industria 4.0

2020-2021

PAStor

Programmable and Adaptable Storage for AI-oriented HPC Ecosystems

2020-2021

ACTPM

Automating Crash-Consistency Testing for Persistent Memory

2020-2021

AIDA

Adaptive, Intelligent and Distributed Assurance Platform

2020-2023

BigHPC

A Management Framework for Consolidated Big Data and HPC

2020-2023

SLSNA

Prestação de Serviços no ambito do projeto SKORR

2020-2021

InterConnect

Interoperable Solutions Connecting Smart Homes, Buildings and Grids

2019-2024

T4CDTKC

Training 4 Cotec, Digital Transformation Knowledge Challenge - Elaboração de Programa de Formação “CONHECER E COMPREENDER O DESAFIO DAS TECNOLOGIAS DE TRANSFORMAÇÃO DIGITAL”

2019-2021

CLOUD4CANDY

Cloud for CANDY

2019-2019

HADES

Sistemas descentralizados confiáveis e escaláveis suportados por hardware

2018-2022

MaLPIS

Aprendizagem Automática para Deteção de Ataques e Identificação de Perfis Segurança na Internet

2018-2022

SKORR

Advancing the Frontier of Social Media Management Tools

2018-2021

DaVinci

Architecturas distribuídas: variabilidade e interação de sistemas ciber-físicos

2018-2022

SAFER

Verificação de segurança para software robótico

2018-2021

KLEE

Modelação coalgébrica e análise para biologia sintética computacional

2018-2021

InteGrid

Demonstration of INTElligent grid technologies for renewables INTEgration and INTEractive consumer participation enabling INTEroperable market solutions and INTErconnected stakeholders

2017-2020

Lightkone

Lightweight Computation for Networks at the Edge

2017-2019

CloudDBAppliance

European Cloud In-Memory Database Appliance with Predictable Performance for Critical Applications

2016-2019

Cloud-Setup

PLATAFORMA DE PREPARAÇÃO DE CONTEÚDOS AUDIOVISUAIS PARA INGEST NA CLOUD

2016-2019

GSL

GreenSoftwareLab: Computação Verde como uma Disciplina de Engenharia

2016-2019

CORAL-TOOLS

CORAL - Sustainable Ocean Exploitation: Tools and Sensors

2016-2018

SafeCloud

Secure and Resilient Cloud Architecture

2015-2018

NanoStima-RL1

NanoSTIMA - Macro-to-Nano Human Sensing Technologies

2015-2019

NanoStima-RL3

NanoSTIMA - Health data infrastructure

2015-2019

SMILES

TEC4Growth - RL SMILES - Smart, Mobile, Intelligent and Large scale Sensing and analytics

2015-2019

UPGRID

Real proven solutions to enable active demand and distributed generation flexible integration, through a fully controllable LOW Voltage and medium voltage distribution grid

2015-2017

LeanBigData

Análise Integrada e Visual de Big Data Ultra-escalável e Ultra-eficiente

2014-2017

Practice

Ferramentas de Preservação de Privacidade na Cloud

2013-2016

CoherentPaaS

PaaS Rica e Coerente com um Modelo de Programação Comum

2013-2016

Equipa
001

Laboratório

CLOUDinha

Publicações

HASLab Publicações

Ler todas as publicações

2025

Leakage-Free Probabilistic Jasmin Programs

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

Publicação
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

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

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

Publicação
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING

Abstract
[No abstract available]

2025

Introduction to the Special Collection from FACS 2022

Autores
Tapia Tarifa, SL; Proença, J; Oliveira, JN;

Publicação
Formal Aspects Comput.

Abstract
[No abstract available]

2025

How much is in a square? Calculating functional programs with squares

Autores
Oliveira, JN;

Publicação
JOURNAL OF FUNCTIONAL PROGRAMMING

Abstract
Experience in teaching functional programming (FP) on a relational basis has led the author to focus on a graphical style of expression and reasoning in which a geometric construct shines: the (semi) commutative square. In the classroom this is termed the magic square (MS), since virtually everything that we do in logic, FP, database modeling, formal semantics and so on fits in some MS geometry. The sides of each magic square are binary relations and the square itself is a comparison of two paths, each involving two sides. MSs compose and have a number of useful properties. Among several examples given in the paper ranging over different application domains, free-theorem MSs are shown to be particularly elegant and productive. Helped by a little bit of Galois connections, a generic, induction-free theory for ${\mathsf{foldr}}$ and $\mathsf{foldl}$ is given, showing in particular that ${\mathsf{foldl} \, {{s}}{}\mathrel{=}\mathsf{foldr}{({flip} \unicode{x005F}{s})}{}}$ holds under conditions milder than usually advocated.

2025

CRDV: Conflict-free Replicated Data Views

Autores
Faria, N; Pereira, J;

Publicação
Proc. ACM Manag. Data

Abstract
There are now multiple proposals for Conflict-free Replicated Data Types (CRDTs) in SQL databases aimed at distributed systems. Some, such as ElectricSQL, provide only relational tables as convergent replicated maps, but this omits semantics that would be useful for merging updates. Others, such as Pg\_crdt, provide access to a rich library of encapsulated column types. However, this puts merge and query processing outside the scope of the query optimizer and restricts the ability of an administrator to influence access paths with materialization and indexes. Our proposal, CRDV, overcomes this challenge by using two layers implemented as SQL views: The first provides a replicated relational table from an update history, while the second implements varied and rich types on top of the replicated table. This allows the definition of merge semantics, or even entire new data types, in SQL itself, and enables global optimization of user queries together with merge operations. Therefore, it naturally extends the scope of query optimization and local transactions to operations on replicated data, can be used to reproduce the functionality of common CRDTs with simple SQL idioms, and results in better performance than alternatives.

Factos & Números

68Investigadores

2016

0Capítulos de livros

2020

1Contratados de I&D

2020

Contactos