Detecting Unsafe Code-Patterns Using Computational Tree Logic
Authors
Aaen, Christoffer Bigum ; Eriksen, Mikkel Østergaard ; Klausen, Mathias Karstoft
Term
4. term
Education
Publication year
2023
Pages
74
Abstract
This project develops a way to represent programs in NuSMV syntax using MiniMC, a symbolic execution engine (it explores many possible execution paths without fixed inputs). The goal is to enable CTL analysis through a NuSMV implementation inside MiniMC; CTL is a temporal logic used to reason about program behavior over time. For programs where we do not need to inspect register contents, our approach can spot basic vulnerable patterns. Notably, it detects a fork bomb with high accuracy and also identifies a double-free vulnerability (freeing the same memory twice). However, the solution cannot find all vulnerable patterns. A main reason is MiniMC's limitations: it cannot load or store pointers on the heap (dynamically allocated memory), which hides some patterns. In addition, MiniMC's use of LLVM IR (an intermediate code representation) and SSA form (each variable assigned once) makes it difficult to detect patterns that operate on registers. We conclude that the solution can detect some vulnerabilities, but not all.
Dette projekt udvikler en måde at repræsentere programmer i NuSMV-syntaks ved hjælp af MiniMC, en motor til symbolsk eksekvering (en teknik der udforsker mange mulige kørselsveje uden konkrete input). Målet er at køre CTL-analyse via en NuSMV-implementering i MiniMC; CTL er en temporal logik, der bruges til at beskrive et programs adfærd over tid. For programmer, hvor vi ikke behøver at inspicere indholdet af registre, kan vores tilgang finde simple sårbarhedsmønstre. Vi kan blandt andet opdage en fork-bombe med høj nøjagtighed og også identificere en double-free sårbarhed (den samme hukommelse frigives to gange). Samtidig kan løsningen ikke finde alle sårbarheder. En hovedårsag er begrænsninger i MiniMC: den kan ikke læse eller skrive pegere på heap'en (dynamisk hukommelse), hvilket gør nogle mønstre usynlige. Derudover gør brugen af LLVM IR (et mellemliggende kodeformat) og SSA-form (hvor hver variabel kun tildeles én gang) det vanskeligt at opdage mønstre, der afhænger af registre. Vi konkluderer, at løsningen kan opdage visse sårbarheder, men ikke alle.
[This apstract has been rewritten with the help of AI based on the project's original abstract]
Keywords