Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

analyzer: Allow snprintf(NULL, 0, ...) (#221). #286

Merged

Conversation

ivanperez-keera
Copy link
Collaborator

IKOS currently considers that the first argument of snprintf should never be null. However, a first argument null is allowed when the second argument is zero.

This commit introduces a check for that second value; only when it is not the literal zero is the first argument checked. The check applies to the null dereference checker, the buffer overflow checker and the numerical execution engine.

This check is not perfect: the second argument could also be a variable with the value or function call that returns zero. However, since passing the literal zero is the most common scenario, we check for that case for now.

IKOS currently considers that the first argument of snprintf should
never be null. However, a first argument null is allowed when the second
argument is zero.

This commit introduces a check for that second value; only when it is
not the literal zero is the first argument checked. The check applies to
the null dereference checker, the buffer overflow checker and the
numerical execution engine.

This check is not perfect: the second argument could also be a variable
with the value or function call that returns zero. However, since
passing the literal zero is the most common scenario, we check for that
case for now.
@ivanperez-keera
Copy link
Collaborator Author

ivanperez-keera commented Sep 28, 2024

I checked that this fixes the issue with the following dockerfile and test files:

# Based on image by Maxime Arthaud
FROM debian:latest
MAINTAINER Ivan Perez <ivan.perezdominguez@nasa.gov>
ARG njobs=2
ARG build_type=Release

# Upgrade
RUN apt-get update
RUN apt-get upgrade -y

# Refresh cache
RUN apt-get update

# Install all dependencies
RUN apt-get install --yes gcc g++ cmake libgmp-dev libboost-dev libboost-filesystem-dev \
    libboost-thread-dev libboost-test-dev python3 python3-pygments libsqlite3-dev libtbb-dev \
    libz-dev libedit-dev llvm-14 llvm-14-dev llvm-14-tools clang-14 \
    git python3.11-venv python3-pip

RUN apt install --yes vim

# Add ikos source code
WORKDIR /root
RUN git clone -b develop-snprintf-null https://github.com/NASA-SW-VnV/ikos

# Build ikos
RUN rm -rf /root/ikos/build && mkdir /root/ikos/build
WORKDIR /root/ikos/build
ENV MAKEFLAGS "-j$njobs"
RUN cmake \
        -DCMAKE_INSTALL_PREFIX="/opt/ikos" \
        -DCMAKE_BUILD_TYPE="$build_type" \
        -DLLVM_CONFIG_EXECUTABLE="/usr/lib/llvm-14/bin/llvm-config" \
        ..
RUN make
RUN make install

# Add ikos to the path
ENV PATH "/opt/ikos/bin:$PATH"

# Done
WORKDIR /

First test (should pass)

Test file:

#include <stdio.h>

int main(void) {
    snprintf(NULL, 0, "%d", 123);
    return 0;
}

Output:

$ ikos test.c 
[*] Compiling test.c
[*] Running ikos preprocessor
[*] Running ikos analyzer
[*] Translating LLVM bitcode to AR
[*] Running liveness analysis
[*] Running widening hint analysis
[*] Running interprocedural value analysis
[*] Analyzing entry point 'main'
[*] Checking properties for entry point 'main'

# Time stats:
clang        : 0.613 sec
ikos-analyzer: 0.089 sec
ikos-pp      : 0.173 sec

# Summary:
Total number of checks                : 3
Total number of unreachable checks    : 0
Total number of safe checks           : 3
Total number of definite unsafe checks: 0
Total number of warnings              : 0

The program is SAFE

# Results
No entries.

Second test (should fail)

Test file:

#include <stdio.h>

int main(void) {
    snprintf(NULL, 1, "%d", 123);
    return 0;
}

Output:

$ ikos test.c 
[*] Compiling test.c
[*] Running ikos preprocessor
[*] Running ikos analyzer
[*] Translating LLVM bitcode to AR
[*] Running liveness analysis
[*] Running widening hint analysis
[*] Running interprocedural value analysis
[*] Analyzing entry point 'main'
[*] Checking properties for entry point 'main'

# Time stats:
clang        : 0.040 sec
ikos-analyzer: 0.010 sec
ikos-pp      : 0.007 sec

# Summary:
Total number of checks                : 3
Total number of unreachable checks    : 1
Total number of safe checks           : 1
Total number of definite unsafe checks: 1
Total number of warnings              : 0

The program is definitely UNSAFE

# Results
test.c: In function 'main':
test.c:4:5: error: first argument is null
    snprintf(NULL, 1, "%d", 123);
    ^
test.c: In function 'main':
test.c:5:5: unreachable: code is dead
    return 0;
    ^

@ivanperez-keera ivanperez-keera merged commit 9963a3f into NASA-SW-VnV:master Sep 28, 2024
2 checks passed
@ivanperez-keera ivanperez-keera deleted the develop-snprintf-null branch September 28, 2024 18:09
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant