Cookies
Usamos cookies para melhorar nosso site e a sua experiência. Ao continuar a navegar no site, você aceita a nossa política de cookies. Ver mais
Aceitar Rejeitar
  • Menu
Factos & Números
000
Apresentação

Laboratório de Software Confiável

No HASLab, o nosso trabalho incide sobre o desenho e a implementação de sistemas de software confiável: softwarecorrect by design, resiliente perante falhas e ataques maliciosos. Com vista a cumprir a nossa missão, operamos no cluster das Ciências da Computação, e as nossas atividades de investigação seguem uma abordagem concreta a três grandes áreas: Engenharia de Software, Sistemas Distribuídos, e Criptografia e Segurança da Informação.

Os principais contributos do HASLab nas dimensões acima referidas vão desde a investigação fundamental em métodos e algoritmos formais, até a investigação aplicada ao desenvolvimento de ferramentas e middleware, com vista a responder aos principais desafios do mundo atual, decorrentes da colaboração, a longo prazo, com a indústria.

Engenharia de Software - exploramos métodos, técnicas e ferramentas para o desenvolvimento de software, podendo este ser introduzido nas funcionalidades internas de certos componentes, na sua configuração junto de outros componentes, e também na interação com o usuário.

Sistemas Distribuídos – um dos nossos objetivos é aperfeiçoar a confiabilidade e escalabilidade de software, explorando propriedades inerentes à distribuição e replicação de sistemas computacionais.

Criptografia e Segurança da Informação - visamos minimizar a vulnerabilidade dos componentes de software a ataques maliciosos, através da implementação de estruturas e protocolos criptográficos, cujas propriedades de segurança são formalmente comprovadas.

Através de uma abordagem multidisciplinar, assente em princípios teóricos comprovados, pretendemos disponibilizar soluções – fundamentos teóricos, métodos, linguagens, ferramentas, etc. - para o desenvolvimento de sistemas TIC integrais, com garantias concretas aos seus proprietários e utilizadores. As principais áreas de aplicação da investigação levada a cabo no HASLab incluem o desenvolvimento de sistemas de software essenciais para garantir a segurança e a proteção, a operacionalização de infraestruturas da nuvem, e a gestão e o processamento de BigData, preservando a sua privacidade.

Últimas Notícias
Informática

INESC TEC coorganiza workshop sobre Inteligência Artificial aplicada a testes de software

O INESC TEC coorganizou o workshop AIST 2021 – International Workshop on Artificial Intelligence in Software Testing, no âmbito da IEEE International Conference on Software Testing (ICST 2021), e dedicado à Inteligência Artificial para testes de software. O evento decorreu online, no dia 12 de abril, e contou com mais de 20 participantes.  

07 maio 2021

Informática

Projeto INESC TEC vence Prémio IN3+

O projeto IDINA – Identidade Digital Inclusiva Não Autoritativa, liderado pelo Laboratório de Software Confiável (HASLAb) do INESC TEC, é o vencedor do Prémio IN3+, promovido pela Imprensa Nacional – Casa da Moeda S.A. (INCM), no valor de 600 mil euros. O IDINA pretende criar uma plataforma de identificação do cidadão eficaz e inclusiva, em países que não possuem sistemas centrais de identificação (infraestruturas de registo civil), para todos os cidadãos.

30 março 2021

Informática

Projeto CoronaSurveys distinguido em concurso internacional

O projeto CoronaSurveys, que pretende determinar a incidência da pandemia em vários países, foi distinguido no “XPRIZE Pandemic Response Challenge” com uma menção honrosa e um prémio no valor de 3 mil euros em crédito AWS (Amazon Web Services)­­­­­.

24 março 2021

Informática

Projeto INESC TEC coloca NAU 21 nas 10 melhores empresas de Insurtech da Europa

Em parceria com o INESC TEC, o desenvolvimento da plataforma SIS permitiu à NAU21, empresa incubada no UPTEC, ser distinguida pela revista Insurance CIO Outlook, como uma das 10 das melhores empresas de Insurtech da Europa. Esta plataforma pretende revolucionar a forma como qualquer pessoa lida com os seguros, tornando os processos mais simples, rápidos e diretos.

05 março 2021

Informática

Projeto do INESC TEC nos cinco finalistas do Prémio IN3+

O projeto IDINA, Identidade Digital Inclusiva Não-Autoritativa, é um dos projetos finalistas da terceira edição do Prémio IN3+, uma iniciativa que pretende apoiar a geração de novas ideias, promovida pela Imprensa Nacional-Casa da Moeda (INCM).  

22 fevereiro 2021

Tópicos de Interesse
033

Projetos Selecionados

PassCert

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

2021-2022

RISC2

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

2021-2023

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

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

2020-2021

Collaboration

Collaborative Visual Development

2020-2021

AIDA

Adaptive, Intelligent and Distributed Assurance Platform

2020-2022

BigHPC

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

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

CLOUD4CANDY

Cloud for CANDY

2019-2019

HADES

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

2018-2021

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

2021

A deductive reasoning approach for database applications using verification conditions

Autores
Alam, MI; Halder, R; Pinto, JS;

Publicação
JOURNAL OF SYSTEMS AND SOFTWARE

Abstract
Deductive verification has gained paramount attention from both academia and industry. Although intensive research in this direction covers almost all mainstream languages, the research community has paid little attention to the verification of database applications. This paper proposes a comprehensive set of Verification Conditions (VCs) generation techniques from database programs, adapting Symbolic Execution, Conditional Normal Form, and Weakest Precondition. The validity checking of the generated VCs for a database program determines its correctness w.r.t. the annotated database properties. The developed prototype DBverify based on our theoretical foundation allows us to instantiate VC generation from PL/SQL codes, yielding to detailed performance analysis of the three approaches under different circumstances. With respect to the literature, the proposed approach shows its competence to support crucial SQL features (aggregate functions, nested queries, NULL values, and set operations) and the embedding of SQL codes within a host imperative language. For the chosen set of benchmark PL/SQL codes annotated with relevant properties of interest, our experiment shows that only 38% of procedures are correct, while 62% violate either all or part of the annotated properties. The primary cause for the latter case is mostly due to the acceptance of runtime inputs in SQL statements without proper checking.

2021

Ranking programming languages by energy efficiency

Autores
Pereira, R; Couto, M; Ribeiro, F; Rua, R; Cunha, J; Fernandes, JP; Saraiva, J;

Publicação
Science of Computer Programming

Abstract
This paper compares a large set of programming languages regarding their efficiency, including from an energetic point-of-view. Indeed, we seek to establish and analyze different rankings for programming languages based on their energy efficiency. The goal of being able to rank programming languages based on their energy efficiency is both recent, and certainly deserves further studies. We have taken rigorous and strict solutions to 10 well defined programming problems, expressed in (up to) 27 programming languages, from the well known Computer Language Benchmark Game repository. This repository aims to compare programming languages based on a strict set of implementation rules and configurations for each benchmarking problem. We have also built a framework to automatically, and systematically, run, measure and compare the energy, time, and memory efficiency of such solutions. Ultimately, it is based on such comparisons that we propose a series of efficiency rankings, based on single and multiple criteria. Our results show interesting findings, such as how slower/faster languages can consume less/more energy, and how memory usage influences energy consumption. We also present a simple way to use our results to provide software engineers and practitioners support in deciding which language to use when energy efficiency is a concern. In addition, we further validate our results and rankings against implementations from a chrestomathy program repository, Rosetta Code., by reproducing our methodology and benchmarking system. This allows us to understand how the results and conclusions from our rigorously and well defined benchmarked programs compare to those based on more representative and real-world implementations. Indeed our results show that the rankings do not change apart from one programming language. © 2021 Elsevier B.V.

2021

Fuzzy Automata as Coalgebras

Autores
Liu, A; Wang, S; Barbosa, LS; Sun, M;

Publicação
MATHEMATICS

Abstract
The coalgebraic method is of great significance to research in process algebra, modal logic, object-oriented design and component-based software engineering. In recent years, fuzzy control has been widely used in many fields, such as handwriting recognition and the control of robots or air conditioners. It is then an interesting topic to analyze the behavior of fuzzy automata from a coalgebraic point of view. This paper models different types of fuzzy automata as coalgebras with a monad structure capturing fuzzy behavior. Based on the coalgebraic models, we can define a notion of fuzzy language and consider several versions of bisimulation for fuzzy automata. A group of combinators is defined to compose fuzzy automata of two branches: state transition and output function. A case study illustrates the coalgebraic models proposed and their composition.

2021

Secure Conflict-free Replicated Data Types

Autores
Barbosa, M; Ferreira, B; Marques, JC; Portela, B; Preguiça, NM;

Publicação
ICDCN '21: International Conference on Distributed Computing and Networking, Virtual Event, Nara, Japan, January 5-8, 2021.

Abstract

2021

GenoDedup: Similarity-Based Deduplication and Delta-Encoding for Genome Sequencing Data

Autores
Cogo, V; Paulo, J; Bessani, A;

Publicação
IEEE Transactions on Computers

Abstract

Teses Orientadas

2020

Extending Conflict Free Replicated Data Types Fault Models

Autor
Houssam Ahmad Yactine

Instituição
UP-FCUP

2020

Peer-production and Technology-enhanced Collaborative Teaching and Learning (Models, Methods and Framework)

Autor
sara dos Santos Fernandes

Instituição
UP-FCUP

2020

TrustZone based Attestation in Secure Runtime Verification for Embbeded Systems

Autor
Miguel Miranda Quaresma

Instituição
UM

2020

Suporte ao desenvolvimento de aplicações críticas em sistemas embebidos

Autor
Lisandra Maria Pereira da Silva

Instituição
UM

2020

Prototipagem de Interfaces

Autor
Rafael Braga Gomes da Costa

Instituição
UM

Factos & Números

4Artigos em revistas indexadas

2020

14Artigos em conferências indexadas

2020

0Capítulos de livros

2020

Contactos