Filipe Marques

2024

1. Programming

   Owi: Performant Parallel Symbolic Execution Made Easy, an Application to WebAssembly

   Léo Andrès, Filipe Marques, Arthur Carcano, and 3 more authors

   The Art, Science, and Engineering of Programming, Oct 2024

   Bib PDF

   @article{andres2024owi,
     title = {{Owi: Performant Parallel Symbolic Execution Made Easy, an
                Application to WebAssembly}},
     author = {Andr{\`e}s, L{\'e}o and Marques, Filipe and Carcano, Arthur and Chambart, Pierre and Fragoso Santos, Jos{\'e} and Filli{
                 \^a}tre, Jean-Christophe},
     url = {https://hal.science/hal-04627413},
     journal = {{The Art, Science, and Engineering of Programming}},
     publisher = {{aosa, Inc.}},
     volume = {9},
     number = {2},
     year = {2024},
     month = oct,
     keywords = {WebAssembly ; Wasm ; Owi ; Symbolic execution ; Bug Finding ; Rust
                   ; C ; Cross-language ; Interpreter ; Monad ; Multi-core ; Parallel},
     hal_id = {hal-04627413},
     hal_version = {v2}
   }

2022

1. ECOOP

   Concolic Execution for WebAssembly

   Filipe Marques, José Fragoso Santos, Nuno Santos, and 1 more author

   In 36th European Conference on Object-Oriented Programming (ECOOP 2022), Oct 2022

   Abs Bib PDF

   WebAssembly (Wasm) is a new binary instruction format that allows targeted compiled code written in high-level languages to be executed by the browser’s JavaScript engine with near-native speed. Despite its clear performance advantages, Wasm opens up the opportunity for bugs or security vulnerabilities to be introduced into Web programs, as pre-existing issues in programs written in unsafe languages can be transferred down to cross-compiled binaries. The source code of such binaries is frequently unavailable for static analysis, creating the demand for tools that can directly tackle Wasm code. Despite this potentially security-critical situation, there is still a noticeable lack of tool support for analysing Wasm binaries. We present WASP, a symbolic execution engine for testing Wasm modules, which works directly on Wasm code and was built on top of a standard-compliant Wasm reference implementation. WASP was thoroughly evaluated: it was used to symbolically test a generic data-structure library for C and the Amazon Encryption SDK for C, demonstrating that it can find bugs and generate high-coverage testing inputs for real-world C applications; and was further tested against the Test-Comp benchmark, obtaining results comparable to well-established symbolic execution and testing tools for C.

   @inproceedings{marques2022wasp,
     author = {Marques, Filipe and Fragoso Santos, Jos{\'e} and Santos, Nuno and Ad{\~a}o, Pedro},
     title = {{Concolic Execution for WebAssembly}},
     booktitle = {36th European Conference on Object-Oriented Programming (ECOOP
                    2022)},
     pages = {11:1--11:29},
     series = {Leibniz International Proceedings in Informatics (LIPIcs)},
     isbn = {978-3-95977-225-9},
     issn = {1868-8969},
     year = {2022},
     volume = {222},
     editor = {Ali, Karim and Vitek, Jan},
     publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
     address = {Dagstuhl, Germany},
     url = {https://drops.dagstuhl.de/opus/volltexte/2022/16239},
     urn = {urn:nbn:de:0030-drops-162394},
     doi = {10.4230/LIPIcs.ECOOP.2022.11},
     annote = {Keywords: Concolic Testing, WebAssembly, Test-Generation, Testing C
                 Programs}
   }