Projects Currently Active

Software Defined Networks (SDN) is a powerful paradigm that allows administrators to have a global view of the network and configure data flows using central controllers without the need to manually configure switches. As all new technologies, SDN can be used to mitigate known attacks, but it also has vulnerabilities that can be exploited. This project is interested in mitigating Distributed Denial of Service (DDoS) Attacks in SDN networks. DDoS attacks remain a great threat to the Internet. The recent years have witnessed an increa- sing variety on the types and increasing sizes of DDoS attacks. New attacks, called Application- Layer DDoS (AppDDoS), exploit application layer protocols (HTTP and SIP) instead of trans- port layer protocols (ICMP, UDP, TCP). Amplification Attacks (AmpDDoS) exploit the networ- king infrastructure (e.g, NTP servers) to carry out huge volume attacks (in the order of Gpbs). Finally, SDN-DDoS attacks have exploited SDN vulnerabilities to carry out new attacks in SDN. In this project, we will extend to SDN our methods for mitigating low-rate AppDDoS based on selective strategies developed in the scope of the project GT-ACTIONS together with our partner the RNP. Exploiting the fact that SDNs have a global view of the network, we can mitigate High-Rate AppDDoS attacks and AmpDDoS. On the other hand, by using selective strategies, we can mitigate SDN-DDoS that exploit SDN vulnerabilities such as Rule Inundation Attack. SecureSDN will propose, model, implement, simulate and validate in SDNs defenses using selective strategies.

Funded by fapesp

Members: UFPB, RNP, ACTIONS Security

Developing avionic components remains a challenge as there are many players involved using different technologies for modeling and developing products. The main objective of this project is to study the use of Model Based Engineering to help the development process.

Funded by BMWi
Members: Number of industry partners: Airbus, Diehl, Liebherr, Nordmicro, Philotec, Silva Atena, fortiss

Computational systems often are restricted by differents types/modes aspects. For example, web-servers are restricted by the amount of memory allocated, or cyber-physical systems by the energy available. This project aims to build the foundations for specifying and analysing such systems. We consider the use of quantitative constraints, investigating how to automate verification, and apply our techniques to the most varied systems.

Funded by CNPq

Distributed Denial of Service (DDoS) attacks remain among the most dangerous and noticeable attacks on the Internet. Differently from previous attacks, many recent DDoS attacks have not been carried out over the network layer, but over the application layer. The main difference is that in the latter, an attacker can target a particular application of the server, while leaving the remaining applications still available, thus generating less traffic and being harder to detect. This project’s main objective is to develop a framework for building defenses against such attacks.

Funded by Rede Nacional de Ensino e Pesquisa
Members: Prof. Iguatemi Fonseca; Prof. Moises Ribeiro; Prof. Helio Waldman

Old Projects

In a collaborative system, agents work together in order to achieve a common goal, but at the same time, try to avoid that bad things happen, that is, bad states are reached. An example of such a collaboration is a clinical investigation (CI), which is a set of procedures in medical research and drug development, whose goal is to test a new drug or other intervention on human subjects. In a CI, subjects, nurses, doctors, hospital administrators, regulatory agencies, clinical research organizations (CRO), and pharmaceutical companies (Sponsors) collaborate in order to test the effectiveness of the experimental drug, so that it can be approved by public agencies, such as the Food and Drug Administration (FDA). This project’s mais objective is to develop a formal executable semantics for Regulated Collaborative Systems which is amenable to formal verification tools.

Funded by Capes
Members: Prof. Carolyn Talcott; Prof. Andre Scedrov; Prof. Max Kanovich; Prof. Kenneth John Gollob; Prof. Walderez Ornelas Dutra.

Time is important for setting the rules and goals of a successful collaboration. This project’s main goal is to develop a framework for the specification of complex collaborative systems with explicit time; investigate the foundational differences of such models; and apply such framework.

Funded by CNPq Members: Prof. Carolyn Talcott; Prof. Andre Scedrov; Prof. Max Kanovich; Prof. Elaine Pimentel; Prof. Carlos Olarte.

As the world gets more interconnected and softwares more distributed, it becomes more important that computer scientists and engineers are able to correctly model and formally specify concurrent processes. As logic and proof theory have a long tradition on dealing with formal languages and provide powerful tools to reason about them, they have been successfully used to model computation. In particular, the recent years have witnessed an increase on our understanding of the application of proof theory, in the context of the computation-as-deduction paradigm, as a framework to specify and reason about computation systems. The main objective of this project is to exploit recent proof theoretic developments to provide a general framework and reasoning techniques for concurrency. The scien- tific impact of the project will be twofold: on one hand, deep proof theoretic insights will be required in order to propose such framework and techniques. On the other hand, not only existing concepts in concurrency shall be given proof theoretic expla- nations, but also new concepts shall emerge, leading towards a general proof theory for concurrency.

Funded by the Alexander von Humboldt Foundation
Members: Prof. Martin Hofmann