A master thesis from Aalborg University
Detecting Unsafe Code-Patterns Using Computational Tree Logic
Term
4. term
Education
Publication year
2023
Submitted on
2023-06-15
Pages
74 pages
Abstract
This project presents a solution to model a program in NuSMV syntax using MiniMC. MiniMC is a symbolic execution engine, and we aim to perform Computational Temporal Logic (CTL) analysis using a NuSMV implementation in MiniMC. We found that for programs where we do not need to need to verify the contents of registers, we can detect primitive vulnerable patterns in the program. Among the notable results are that we can detect a fork bomb with great accuracy as well as detect a double-free vulnerability. We conclude that the solution is able to detect some vulnerable patterns in programs, but that it is not able to detect all vulnerable patterns. We note that mostly due to limitations in MiniMC we are not able to detect all vulnerable patterns, as MiniMC is not able to load and store pointers on the heap. Furthermore, due to MiniMC using LLVM IR and subsequently SSA form, detecting patterns operating on registers is difficult.
Keywords
Documents
Colophon: This page is part of the AAU Student Projects portal, which is run by Aalborg University. Here, you can find and download publicly available bachelor's theses and master's projects from across the university dating from 2008 onwards. Student projects from before 2008 are available in printed form at Aalborg University Library.
If you have any questions about AAU Student Projects or the research registration, dissemination and analysis at Aalborg University, please feel free to contact the VBN team. You can also find more information in the AAU Student Projects FAQs.