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

Novo membro na coordenação do HASLab

Na reunião de Conselho de Administração do INESC TEC, que aconteceu no dia 7 de maio, foi comunicada a nomeação de António Luís Sousa para a co-coordenação do Laboratório de Software Confiável (HASLab), funções que exercerá em conjunto com Alcino Cunha, que se mantém como co-coordenador do Centro.

17 junho 2019

Terminou projeto que potencia criação de apps empresariais com dados não-relacionais

RADicalize BigData, um projeto de prestação de serviços com a OutSystems, levado a cabo pelo Laboratório de Software Confiável (HASLab) do INESC TEC, permitiu desenvolver uma forma de integrar dados de fontes Big Data em aplicações empresariais usando uma abordagem low-code, compatível com a plataforma OutSystems.

14 junho 2019

A mais recente spin-off do INESC TEC chama-se Keyruptive

A mais recente spin-off do INESC TEC chama-se Keyruptive e atua na área da segurança informática. Nasceu em Braga, fruto do trabalho de vários anos de um grupo de investigadores do Laboratório de Software Confiável (HASLab) do INESC TEC, e já tem uma solução tecnológica para apresentar ao mercado, cujo nome é igual ao da empresa agora criada.

13 junho 2019

INESC TEC lidera projeto europeu de 36M€ para digitalização do sistema elétrico

O maior projeto colaborativo europeu aprovado pela Comissão Europeia, ao abrigo do programa de financiamento Horizonte 2020, chama-se InterConnect e vai ser liderado pelo INESC TEC.

04 junho 2019

Empresa CLEARSY visita INESC TEC

Thierry Lecomte, Diretor de Projetos de Investigação e Desenvolvimento da CLEARSY Systems Engineering, visitou o Laboratório de Software Confiável (HASLab) do INESC TEC, em Braga, e a sede do Instituto, no Porto, nos dias 6 e 7 de março.

23 abril 2019

060

Projetos Selecionados

exaSIMPLE

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

2024-2025

Saude24GB

Linha de Saúde 24h da Guiné-Bissau

2024-2024

EPICURE

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

2024-2028

TwinEU

Digital Twin for Europe

2024-2026

HANAMI

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

2024-2026

ENSCOMP3

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

2023-2025

AzDIH

Azores Digital Innovation Hub on Tourism and Sustainability

2023-2025

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

Green_Dat_AI

Energy-efficient AI-ready Data Spaces

2023-2025

EuroCC2

National Competence Centres in the framework of EuroHPC Phase 2

2023-2025

fMP

Formação de Introdução à utilização de recursos HPC (Técnicas básicas de Programação Paralela)

2022-2022

AURORA

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

2022-2023

NewSpacePortugal

Agenda New Space Portugal

2022-2025

ATTRACT_DIH

Digital Innovation Hub for Artificial Intelligence and High-Performance Computing

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

SpecRep

Constraint-based Specification Repair

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

FLEXCOMM

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

2022-2023

STDCNCS

Desenvolvimento de estudo sobre a comunidade de cibersegurança em Portugal, no âmbito do Observatório de Cibersegurança

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

CloudAnalytics4Dams

Gestão de Grandes Quantidades de Dados em Barragens da EDP Produção

2021-2021

PAStor

Programmable and Adaptable Storage for AI-oriented HPC Ecosystems

2020-2021

PFAI4.0

Programa de Formação Avançada Industria 4.0

2020-2021

Collaboration

Collaborative Visual Development

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

AppOwl

Deteção de Mutações Maliciosas no Browser

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

GSL

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

2016-2019

Cloud-Setup

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

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

2023

Generative Adversarial Networks in Healthcare: A Case Study on MRI Image Generation

Autores
Cepa, B; Brito, C; Sousa, A;

Publicação
2023 IEEE 7TH PORTUGUESE MEETING ON BIOENGINEERING, ENBENG

Abstract
Medical imaging, mainly Magnetic Resonance Imaging (MRI), plays a predominant role in healthcare diagnosis. Nevertheless, the diagnostic process is prone to errors and is conditioned by available medical data, which might be insufficient. A novel solution is resorting to image generation algorithms to address these challenges. Thus, this paper presents a Deep Learning model based on a Deep Convolutional Generative Adversarial Network (DCGAN) architecture. Our model generates 2D MRI images of size 256x256, containing an axial view of the brain with a tumor. The model was implemented using ChainerMN, a scalable and flexible framework that enables faster and parallel training of Deep Learning networks. The images obtained provide an overall representation of the brain structure and the tumoral area and show considerable brain-tumor separation. For this purpose, and owing to their previous state-of-the-art results in general image-generation tasks, we conclude that GAN-based models are a promising approach for medical imaging.

2023

General-Purpose Secure Conflict-free Replicated Data Types

Autores
Portela, B; Pacheco, H; Jorge, P; Pontes, R;

Publicação
2023 IEEE 36TH COMPUTER SECURITY FOUNDATIONS SYMPOSIUM, CSF

Abstract
Conflict-free Replicated Data Types (CRDTs) are a very popular class of distributed data structures that strike a compromise between strong and eventual consistency. Ensuring the protection of data stored within a CRDT, however, cannot be done trivially using standard encryption techniques, as secure CRDT protocols would require replica-side computation. This paper proposes an approach to lift general-purpose implementations of CRDTs to secure variants using secure multiparty computation (MPC). Each replica within the system is realized by a group of MPC parties that compute its functionality. Our results include: i) an extension of current formal models used for reasoning over the security of CRDT solutions to the MPC setting; ii) a MPC language and type system to enable the construction of secure versions of CRDTs and; iii) a proof of security that relates the security of CRDT constructions designed under said semantics to the underlying MPC library. We provide an open-source system implementation with an extensive evaluation, which compares different designs with their baseline throughput and latency.

2023

Privacy-Preserving Machine Learning in Life Insurance Risk Prediction

Autores
Pereira, K; Vinagre, J; Alonso, AN; Coelho, F; Carvalho, M;

Publicação
MACHINE LEARNING AND PRINCIPLES AND PRACTICE OF KNOWLEDGE DISCOVERY IN DATABASES, ECML PKDD 2022, PT II

Abstract
The application of machine learning to insurance risk prediction requires learning from sensitive data. This raises multiple ethical and legal issues. One of the most relevant ones is privacy. However, privacy-preserving methods can potentially hinder the predictive potential of machine learning models. In this paper, we present preliminary experiments with life insurance data using two privacy-preserving techniques: discretization and encryption. Our objective with this work is to assess the impact of such privacy preservation techniques in the accuracy of ML models. We instantiate the problem in three general, but plausible Use Cases involving the prediction of insurance claims within a 1-year horizon. Our preliminary experiments suggest that discretization and encryption have negligible impact in the accuracy of ML models.

2023

Caos: A Reusable Scala Web Animator of Operational Semantics

Autores
Proença, J; Edixhoven, L;

Publicação
Coordination Models and Languages - 25th IFIP WG 6.1 International Conference, COORDINATION 2023, Held as Part of the 18th International Federated Conference on Distributed Computing Techniques, DisCoTec 2023, Lisbon, Portugal, June 19-23, 2023, Proceedings

Abstract

2023

Can We Communicate? Using Dynamic Logic to Verify Team Automata

Autores
ter Beek, MH; Cledou, G; Hennicker, R; Proenca, J;

Publicação
FORMAL METHODS, FM 2023

Abstract
Team automata describe networks of automata with input and output actions, extended with synchronisation policies guiding how many interacting components can synchronise on a shared input/output action. Given such a team automaton, we can reason over communication properties such as receptiveness (sent messages must be received) and responsiveness (pending receivesmust be satisfied). Previouswork focused on how to identify these communication properties. However, automatically verifying these properties is non-trivial, as it may involve traversing networks of interacting automata with large state spaces. This paper investigates (1) how to characterise communication properties for team automata (and subsumed models) using test-free propositional dynamic logic, and (2) how to use this characterisation to verify communication properties by model checking. A prototype tool supports the theory, using a transformation to interact with the mCRL2 tool for model checking.

Factos & Números

0Capítulos de livros

2020

14Artigos em conferências indexadas

2020

68Investigadores

2016

Contactos