Cookies Policy
The website need some cookies and similar means to function. If you permit us, we will use those means to collect data on your visits for aggregated statistics to improve our service. Find out More
Accept Reject
  • Menu
Facts & Numbers
000
Presentation

High-Assurance Software

t HASLab, we are focused on the design and implementation of high-assurance software systems: software that is correct by design and resilient to environment faults and malicious attacks. We accomplish our mission within the Computer Science Cluster, anchoring our research on a rigorous approach to three areas of Computer Science: Software Engineering, Distributed Systems, and Cryptography and Information Security.

Our contributions to these areas range from fundamental research on formal methods and algorithms, to applied research on the development of tools and middleware that address real-world demands stemming from long-term collaborations with industry.

Software Engineering – we research methods, techniques and tools for rigorous software development, that can be applied to the internal functionality of a component, its composition with other components, as well as the interaction with the user.

Distributed Systems – we are focused on improving the reliability and scalability of software, by exploring properties inherent to the distribution and replication of computer systems.

Cryptography and Information Security – we aim to minimize the vulnerability of software components to hostile attacks, by deploying structures and cryptographic protocols whose security properties are formally proven.

Through a multidisciplinary approach that is based on solid theoretical foundations, we aim to provide solutions — theory, methods, languages, tools — for the development of complete ICT systems that provide strong guarantees to their owners and users. Prominent application areas of HASLab research include the development of safety and security critical software systems, the operation of secure cloud infrastructures, and the privacy-preserving management and processing of big data.

Latest News
Computer Science

INESC TEC co-organised workshop on Artificial Intelligence applied to software testing

INESC TEC co-organised the workshop AIST 2021 – International Workshop on Artificial Intelligence in Software Testing, within the scope of the IEEE International Conference on Software Testing (ICST2021), dedicated to AI in software testing. The event took place online, on April 12, with more than 20 participants.

07th May 2021

Computer Science

INESC TEC wins IN3 + Award

The project IDINA - Inclusive Non-Authoritative Digital Identity, INESC TEC’s High Assurance Software Laboratory (HASLab) is the winner of the IN3 + Award, promoted by the Portuguese Mint and Official Printing Office (INCM), of €600K. The project aims to create an effective and inclusive identification platform open to all citizens, in countries that do not have central identification systems (civil registration infrastructures).

30th March 2021

Computer Science

CoronaSurveys project acknowledged at international competition

The CoronaSurveys project, which aims to determine the prevalence of the pandemic in several countries, received an honourable mention and a prize of €3K (AWS - Amazon Web Services credits) at the “XPRIZE Pandemic Response Challenge”.

24th March 2021

Computer Science

INESC TEC project places NAU 21 in the top 10 Insurtech companies in Europe

The development of the SIS platform, in partnership with INESC TEC, led to NAU21 – a company incubated at UPTEC – being acknowledged as one of the 10 best Insurtech companies in Europe, according to Insurance CIO Outlook magazine. This platform aims to revolutionise the way people handle insurance-related matters, making processes simpler, faster and more direct.

05th March 2021

Computer Science

INESC TEC project is one of the five finalists of the IN3+ Award

The IDINA project, Inclusive Non-Authoritative Digital Identity, is one of the finalists of the third edition of the IN3+ Award, an initiative that aims to support the development of new ideas, promoted by the Portuguese Mint and Official Printing Office (INCM).

22nd February 2021

Interest Topics
033

Featured Projects

PassCert

PassCert: Exploring the Impact of Formal Verification on the Adoption of Password Security Software

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

HArdware-backed trusted and scalable DEcentralized Systems

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

Distributed architectures: variability and interaction for cyber-physical systems

2018-2022

SAFER

Safery verification for robotic software

2018-2021

KLEE

Coalgebraic modeling and analysis for computational synthetic biology

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: Towards an Engineering Discipline for Green Software

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

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

Ultra-Scalable and Ultra-Efficient Integrated and Visual Big Data Analytics

2014-2017

Practice

Privacy-Preserving Computation in the Cloud

2013-2016

CoherentPaaS

A Coherent and Rich PaaS with a Common Programming Model

2013-2016

Team
001

Laboratory

CLOUDinha

Publications

HASLab Publications

View all Publications

2021

A deductive reasoning approach for database applications using verification conditions

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

Publication
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

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

Publication
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

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

Publication
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

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

Publication
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

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

Publication
IEEE Transactions on Computers

Abstract

Supervised Theses

2020

Extending Conflict Free Replicated Data Types Fault Models

Author
Houssam Ahmad Yactine

Institution
UP-FCUP

2020

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

Author
sara dos Santos Fernandes

Institution
UP-FCUP

2020

TrustZone based Attestation in Secure Runtime Verification for Embbeded Systems

Author
Miguel Miranda Quaresma

Institution
UM

2020

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

Author
Lisandra Maria Pereira da Silva

Institution
UM

2020

Prototipagem de Interfaces

Author
Rafael Braga Gomes da Costa

Institution
UM

Facts & Figures

0Book Chapters

2020

1R&D Employees

2020

68Researchers

2016

Contacts