FenixEdu™

Dissertação

Toward Tool-Independent Summaries for Symbolic Execution EVALUATED

Detalhes: Execução Simbólica é uma técnica de análise de programas que tem sido aplicada com sucesso para encontrar vários tipos de bugs em codebases industriais. Apesar de ser bastante utilizada na prática, esta técnica sofre de duas limitações principais quando aplicada ao código de programas reais: explosão de caminhos e interações com o ambiente. De forma a tratar ambos os problemas, os motores de execução simbólica atuais fazem uso de sumários simbólicos. Estes interagem com o estado simbólico de um determinado programa de forma a simular o comportamento de funções internas e externas sem ter que executá-las simbolicamente. Os sumários simbólicos podem assim ser usados para mitigar o número de caminhos explorados e permitir a análise de chamadas externas. Apesar das suas vantagens, há uma clara falta de mecanismos para compartilhar sumários simbólicos entre diferentes ferramentas bem como para a sua validação uniforme. Neste projeto apresentamos uma metodologia para implementar sumários, independentes de ferramentas, para a linguagem de programação C. Esta metodologia consiste numa API que contém um conjunto de primitivas de reflexão simbólica para manipulação explícita de estados simbólicos de C. Os sumários simbólicos implementados utilizando nossa API podem ser compartilhados entre diferentes ferramentas de execução simbólica, assumindo que estas ferramentas implementam a API proposta. Além disso, por serem escritos diretamente em C, estes sumários podem ser executados simbolicamente como qualquer código C. Desta forma propomos também uma ferramenta de validação de sumários que pode avaliar sistematicamente a correção de um sumário de acordo com a respetiva implementação de referência.
Keywords: Execução Simbólica, Modelação de Runtime, Sumários Simbólicos, Correção de Sumários

Discussão: novembro 23, 2021, 9:0