Hello !

Welcome to my personal page. Currently I am working on my PhD thesis at Institut Polytechnique de Paris under the supervision of Florian Brandner and Lirida Naviner.

My main research interest is on using formal methods to design hardware. My latest experience is on developping memory controllers and cryptographic modules using the Coq proof assistant.

Other areas of expertise are: RISC-V processor design & optimisation, critical and mixed-criticality Real-Time Embedded Systems, DRAM scheduling, static analysis, concurrent programming, trusted execution environements (TEEs), bare metal development & micro-controllers.

I've also developped a few small projects on other topics, such as: AI, distributed systems, cloud, robotics, connected objects, ultra-low-power electronic design, and mobile networks.

Alternative resources

You can download my CV here. You can also visit my Google Scholar page or my Linkedin page.

Education

PhD at Institut Polytechnique de Paris, Paris, France (2020-present). Thesis: Secure Dynamic Memory Hierarchy.
MsC at Télécom Paris & Université Paris-Saclay, Paris, France (2018-2020). Thesis: Implementation of a biometric library in a multi-core Trusted Execution Environment (TEE). GPA: 16.2/20.
BsC in Electrical Engineering at Universidade Federal de Minas Gerais (UFMG), Belo Horizonte, Brazil (2015-2020). Focus on electronics and computer micro-architecture.
Technical Degree in Industrial Automation at Instituto Federal de Minas Gerais (IFMG), Ouro Preto, Brazil (2012-2014).

Professional Experience

Graduate Research Intern at Collins Aerospace (Jan 2023 - Jun 2023) . I have been applying formal methods to verify customised RISC-V microarchitectures -- with a strong focus on security and cryptography.
Intern at Trustonic (Mar 2020 - Sep 2020) . I implemented a biometric library and provided sample-code for fingerprint and face-recognitionin applications in a resource-limited Trusted Execution Environment (TEE). I've also contributed to the TEE by enabling C++ support on the kernel.

Teaching

Teaching assistant at Télécom Paris (2020 - present). I've been in charge of lab assignments for the following courses: SE201, about Computer Architecture; INF103, about Java and GUIs; INF104, about C programming; and INF106, about Operational Systems and Concurrency.

Publications (from most to least recent)

Lisboa Malaquias, F. , Asavoae, M. & Brandner, F. A formal framework to design and prove trustworthy memory controllers. Real-Time Syst (2023). DOI
Lisboa Malaquias, F., Giantamidis, G., Basagiannis, S., Fulvio Rollini, S., & Amundson, I. (2023). Towards a Methodology to Design Provably Secure Cyber-physical Systems. ACM SIGAda Ada Letters, 43(1), 94-99. DOI
Malaquias, Felipe Lisboa, Mihail Asavoae, and Florian Brandner. "From the Standards to Silicon: Formally Proved Memory Controllers." NASA Formal Methods: 15th International Symposium, NFM 2023, Houston, TX, USA, May 16–18, 2023, Proceedings. Cham: Springer Nature Switzerland, 2023. DOI, AAM
(Best Paper Award) Felipe Lisboa Malaquias, Mihail Asavoae, and Florian Brandner. 2022. A Coq Framework for More Trustworthy DRAM Controllers. In Proceedings of the 30th International Conference on Real-Time Networks and Systems (RTNS ’22), June 7–8, 2022, Paris, France. ACM, New York, NY, USA, 11 pages.

Awards and Honors

Best Paper Award (RTNS, 2022).
1st place at the 1st National RISC-V student contest (Paris, France, 2021). Organised by Thales, CNFM, and the GdR SOC2.
CAPES BRAFITEC Excellence Double Degree Fellowship (Belo Horizonte, Brazil, 2018). Granted by CAPES.
1st place at CoRA, the Autonomous Robot Competition (Belo Horizonte, Brazil, 2016). Organised by PETEE, School of Enginering, UFMG. Along with two teamates, I’ve designed a high speed line follower robot. Our robot’s performance granted us first place in the competition. You can check out the video from the championship round here. The software running on it is here.

Research Projects

Superscalar Processor Timing Anomalies Detector. A software written in C to detect timing anomalies in super-scalar processor trace executions.
RISC-V National Competition. My changes on the Ariane processor that awarded my first place on the 1st National RISC-V student contest.

Skills

Proficiency: C, and the Coq Theorem Prover.
Working level: SystemVerilog, Python, C++, Java.
Basic knownledge: Matlab, HTML, CSS, SQL, Haskell, OCaml, F*, UPPALL, TLA+.