Universidade da Beira Interior


INESC Tecnologia e Ciência - INESC TEC




Dimension Data


MaxData-Healthcare Solutions



Keynote:Frontline and backline cyber security readiness. One doesn’t dispense the other.


José Alegria,Head of Cyber Security, Privacy and Business Continuity,PT Portugal José Alegria,Head of Cyber Security, Privacy and Business Continuity
PT Portugal

Chair: Luís Veiga

Abstract: In this talk we will discuss a holistic approach to cyber security incident detection and response, as a complementary layer to more traditional perimeter and asset protection technology. Most organizations still centralize their Cyber Security Operations in a single frontline operational center supported by traditional SIEM (Security Information and Event Management) technology that is reasonably effective at detecting and helping react to frontline incidents like Distributed Denial of Service attacks. However, it is becoming too common that sophisticated attacks use aggressive and “noisy” frontline attacks as a diversion to more surgical but subtle attack vectors. Unfortunately, current SIEM technologies are not so effective at detecting long tail subtle anomalies.

To respond to this asymmetry, and to also better tackle internal threats, we propose that the cyber security function in a large organization should be organized around two separate but collaborative functions: a frontline SOC focused on short tail (from seconds to a few hours) event series where standard SIEM technology works reasonably well and a backline SOC, based on open source DATA SCIENCE related technology, focused on subtle anomaly detection on long tail (from seconds to a few months) event streams.

In this talk, we will discuss a number of development projects at PT Portugal designed to provide operational support to our own backline SOC: PIASA (PT Identity Access Security & Analytics), DAMS (Data Activity Monitoring & Security), POIROT (Permanent Observation and Investigation of Relevant Ongoing Threats) and HIDRA (High performance Infrastructure for Data Research and Analysis). HIDRA is a high performance AMQP/Elastic cluster designed to enable real-time DATA SCIENCE algorithms over long tail event streams in addition to other computational paradigms: classic/OOP (Ruby), actor model (Elixir/Erlang), CEP (Esper/JRuby) and logic programming and constraint handling rules (CHR/YAP).

CV: José Alegria is responsible for Cyber Security, Privacy and Business Continuity at PT Portugal, covering all lines of business: MIS, IT, Telco, and B2B Security Operations Center services. Technologically, he is particularly interested in actor models, real time complex event processing, machine learning and data science and their applications to security. Before PT he was CTO at ONI Telecom, CEO at BanifServ, MIS director at BFE/BBI banks, member of the management teams at IBM and Data General Portugal, and faculty member in Computer Science at the New University of Lisbon. While at IBM Portugal he launched in 1990 IBM Portugal’s Scientific Prize which is still standing after 25 years. He is an alumni from UNL and from the Ohio State University as a Fulbright-Hays scholar.



Keynote:Formal proofs at the interface of algebra, calculus, and algorithms.


Yves Bertot, research at INRIA Yves Bertot, research at INRIA


Chair: Simão Sousa

Abstract:In this talk, I will illustrate a variety of techniques involved in the verification of mathematical results and algorithms that involved combinations of algebra and analysis. Hopefully, this talk will illustrate the extent of what is possible today using interactive theorem provers and make it possible some of the limitations of this technique for developing correct software.

CV: Yves Bertot is a research at Inria. His initial research was devoted to programming environments and then user-interfaces for interactive theorem provers. He then concentrated on studying the expressive power of interactive theorem provers, especially in the context of Type Theory. A notable result in this category is the book he wrote with P. Casteran on the use of the Coq system.

Yves Bertot has studied formal proofs for a wide variety of domains, ranging from programming language semantics, to computational geometry, to numerical computation. Some of his investigation have also applied to formal proofs for pure mathematics. Yves Bertot has participated to a few large scale efforts, including CompCert (a formally verified compiler), Homotopy Type Theory, and the formal verification of the Feit-Thompson theorem (group theory).

Acções do Documento


Universidade da Beira Interior


Faculdade de Ciências da Universidade do Porto


Instituto Superior Técnico


INESC Tecnologia e Ciência - INESC TEC


Inesc ID Lisboa