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

Energy wars - Chrome vs. Firefox: which browser is more energy efficient?

Autores
Macedo, Jd; Aloísio, J; Gonçalves, N; Pereira, R; Saraiva, J;

Publicação
35th IEEE/ACM International Conference on Automated Software Engineering Workshops, ASE Workshops 2020, Melbourne, Australia, September 21-25, 2020.

Abstract

2020

Understanding the Impact of Introducing Lambda Expressions in Java Programs

Autores
de Mendonça, WLM; Fortes, J; Lopes, FV; Marcilio, D; Bonifácio, R; Canedo, ED; Lima, F; Saraiva, J;

Publicação
J. Softw. Eng. Res. Dev.

Abstract

2020

On energy debt: managing consumption on evolving software

Autores
Couto, M; Maia, D; Saraiva, J; Pereira, R;

Publicação
TechDebt '20: International Conference on Technical Debt, Seoul, Republic of Korea, June 28-30, 2020

Abstract
This paper introduces the concept of energy debt: a new metric, reflecting the implied cost in terms of energy consumption over time, of choosing a flawed implementation of a software system rather than a more robust, yet possibly time consuming, approach. A flawed implementation is considered to contain code smells, known to have a negative influence on the energy consumption. Similar to technical debt, if energy debt is not properly addressed, it can accumulate an energy "interest". This interest will keep increasing as new versions of the software are released, and eventually reach a point where the interest will be higher than the initial energy debt. Addressing the issues/smells at such a point can remove energy debt, at the cost of having already consumed a significant amount of energy which can translate into high costs. We present all underlying concepts of energy debt, bridging the connection with the existing concept of technical debt and show how to compute the energy debt through a motivational example. © 2020 ACM.

2020

The Last Mile: High-Assurance and High-Speed Cryptographic Implementations

Autores
Almeida, JB; Barbosa, M; Barthe, G; Gregoire, B; Koutsos, A; Laporte, V; Oliveira, T; Strub, PY;

Publicação
2020 IEEE SYMPOSIUM ON SECURITY AND PRIVACY (SP 2020)

Abstract
We develop a new approach for building cryptographic implementations. Our approach goes the last mile and delivers assembly code that is provably functionally correct, protected against side-channels, and as efficient as handwritten assembly. We illustrate our approach using ChaCha20Poly1305, one of the two ciphersuites recommended in TLS 1.3, and deliver formally verified vectorized implementations which outperform the fastest non-verified code. We realize our approach by combining the Jasmin framework, which offers in a single language features of high-level and low-level programming, and the EasyCrypt proof assistant, which offers a versatile verification infrastructure that supports proofs of functional correctness and equivalence checking. Neither of these tools had been used for functional correctness before. Taken together, these infrastructures empower programmers to develop efficient and verified implementations by "game hopping", starting from reference implementations that are proved functionally correct against a specification, and gradually introducing program optimizations that are proved correct by equivalence checking. We also make several contributions of independent interest, including a new and extensible verified compiler for Jasmin, with a richer memory model and support for vectorized instructions, and a new embedding of Jasmin in EasyCrypt.

2020

Certified Compilation for Cryptography: Extended x86 Instructions and Constant-Time Verification

Autores
Almeida, JB; Barbosa, M; Barthe, G; Laporte, V; Oliveira, T;

Publicação
Progress in Cryptology - INDOCRYPT 2020 - 21st International Conference on Cryptology in India, Bangalore, India, December 13-16, 2020, Proceedings

Abstract
We present a new tool for the generation and verification of high-assurance high-speed machine-level cryptography implementations: a certified C compiler supporting instruction extensions to the x86. We demonstrate the practical applicability of our tool by incorporating it into supercop: a toolkit for measuring the performance of cryptographic software, which includes over 2000 different implementations. We show i. that the coverage of x86 implementations in supercop increases significantly due to the added support of instruction extensions via intrinsics and ii. that the obtained verifiably correct implementations are much closer in performance to unverified ones. We extend our compiler with a specialized type system that acts at pre-assembly level; this is the first constant-time verifier that can deal with extended instruction sets. We confirm that, by using instruction extensions, the performance penalty for verifiably constant-time code can be greatly reduced. © Springer Nature Switzerland AG 2020.

Factos & Números

4Artigos em revistas indexadas

2020

14Artigos em conferências indexadas

2020

1Contratados de I&D

2020

Contactos