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.

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

2020

On the Construction of Multi-valued Concurrent Dynamic Logics

Autores
Gomes, L;

Publicação
DYNAMIC LOGIC: NEW TRENDS AND APPLICATIONS, DALI 2019

Abstract
Dynamic logic is a powerful framework for reasoning about imperative programs. An extension with a concurrent operator, called concurrent propositional dynamic logic (CPDL) [20], was introduced to formalise programs running in parallel. In a different direction, other authors proposed a systematic method for generating multi-valued propositional dynamic logics to reason about weighted programs [15]. This paper presents the first step of combining these two frameworks to introduce uncertainty in concurrent computations. In the proposed framework, a weight is assigned to each branch of the parallel execution, resulting in a (possible) asymmetric parallelism, inherent to the fuzzy programming paradigm [2,23]. By adopting such an approach, a family of logics is obtained, called multi-valued concurrent propositional dynamic logics (GCDL(A)), parametric on an action lattice A specifying a notion of "weight" assigned to program execution. Additionally, the validity of some axioms of CPDL is discussed in the new family of generated logics.

2019

A generalized program verification workflow based on loop elimination and SA form

Autores
Lourenço, CB; Frade, MJ; Pinto, JS;

Publicação
Proceedings of the 7th International Workshop on Formal Methods in Software Engineering, FormaliSE@ICSE 2019, Montreal, QC, Canada, May 27, 2019.

Abstract
This paper presents a minimal model of the functioning of program verification and property checking tools based on (i) the encoding of loops as non-iterating programs, either conservatively, making use of invariants and assume/assert commands, or in a bounded way; and (ii) the use of an intermediate single-assignment (SA) form. The model captures the basic workflow of tools like Boogie, Why3, or CBMC, building on a clear distinction between operational and axiomatic semantics. This allows us to consider separately the soundness of program annotation, loop encoding, translation into SA form, and VC generation, as well as appropriate notions of completeness for each of these processes. To the best of our knowledge, this is the first formalization of a bounded model checking of software technique, including soundness and completeness proofs using Hoare logic; we also give the first completeness proof of a deductive verification technique based on a conservative encoding of invariant-annotated loops with assume/assert in SA form, as well as the first soundness proof based on a program logic. © 2019 IEEE.

2019

Scalable eventually consistent counters over unreliable networks

Autores
Almeida, PS; Baquero, C;

Publicação
DISTRIBUTED COMPUTING

Abstract
Counters are an important abstraction in distributed computing, and play a central role in large scale geo-replicated systems, counting events such as web page impressions or social network likes. Classic distributed counters, strongly consistent via linearisability or sequential consistency, cannot be made both available and partition-tolerant, due to the CAP Theorem, being unsuitable to large scale scenarios. This paper defines Eventually Consistent Distributed Counters (ECDCs) and presents an implementation of the concept, Handoff Counters, that is scalable and works over unreliable networks. By giving up the total operation ordering in classic distributed counters, ECDC implementations can be made AP in the CAP design space, while retaining the essence of counting. Handoff Counters are the first Conflict-free Replicated Data Type (CRDT) based mechanism that overcomes the identity explosion problem in naive CRDTs, such as G-Counters (where state size is linear in the number of independent actors that ever incremented the counter), by managing identities towards avoiding global propagation and garbage collecting temporary entries. The approach used in Handoff Counters is not restricted to counters, being more generally applicable to other data types with associative and commutative operations.

2019

Conflict-Free Replicated Data Types CRDTs

Autores
Preguiça, NM; Baquero, C; Shapiro, M;

Publicação
Encyclopedia of Big Data Technologies.

Abstract

2019

Higher-Order Patterns in Replicated Data Types

Autores
Leijnse, A; Almeida, PS; Baquero, C;

Publicação
Proceedings of the 6th Workshop on Principles and Practice of Consistency for Distributed Data, PaPoC@EuroSys 2019, Dresden, Germany, March 25-28, 2019

Abstract
The design of Conflict-free Replicated Data Types traditionally requires implementing new designs from scratch to meet a desired behavior. Although there are composition rules that can guide the process, there has not been a lot of work explaining how existing data types relate to each other, nor work that factors out common patterns. To bring clarity to the field we explain underlying patterns that are common to flags, sets, and registers. The identified patterns are succinct and composable, which gives them the power to explain both current designs and open up the space for new ones. © 2019 Copyright held by the owner/author(s). Publication rights licensed to ACM.

Factos & Números

68Investigadores

2016

4Artigos em revistas indexadas

2020

0Capítulos de livros

2020

Contactos