prosyslab-classroom / cs348-information-security

61 stars 10 forks source link

[Question][Hw5] Some questions about homework 5 #130

Closed h2oche closed 3 years ago

h2oche commented 3 years ago

Hello.

About homework 5, I have some questions.

  1. Should we implement meet operator in value domain? It seems that meet operator is not used within our homework.
  2. What is the semantics of sanitizer(x) in sign analysis? Is it top?
  3. Can we change the implementation of functions in Utils? Specifically, I want to change the implementation of flip_pred. As I understand, it seems that functionality of filp_pred is just to change the direction of comparator. However, it changes == to != and != to ==, so I want to fix this.
  4. In taint analysis, does filter operation have effect of the abstract value? For example, in below program, argument of sink should be regarded as tainted?
    int x = source();
    if (x == 0) sink(x); // x tainted?
  5. There seems to have some build/configuration issue in Travis CI. Should we care about this?

Finally, I think there is some mistakes in our test script. If we just run make test in the base directory, it doesn't work. It works only after I fixed test/dune file. The change is as follows:

- (run ../analyzer example1.ll))))
+ (run ../analyzer sign example1.ll))))
- (run ../analyzer example2.ll))))
+ (run ../analyzer sign example2.ll))))
- (run ../analyzer example3.ll))))
+ (run ../analyzer sign example3.ll))))
KihongHeo commented 3 years ago

Thanks for starting good discussion.

  1. I showed the usage of meet in the lecture. If you have a different thought, think about your design a bit more carefully. Doesn't your design implicitly subsume meet?

  2. Top.

  3. It is up to you.

  4. Let us assume that conditional statements do not filter tainted values. Only sanitizer can filter.

  5. Ignore Travis. That's obsolete.

  6. Regarding dune, thanks for reporting the issue. You are right. In addition, please append the following lines.

    +(rule
    + (deps example4.ll)
    + (action
    +  (with-stdout-to
    +   example4.output
    +   (run ../analyzer taint example4.ll))))
    +
    +(rule
    + (alias runtest)
    + (action
    +  (diff example4.expected example4.output)))
    +
    +(rule
    + (deps example5.ll)
    + (action
    +  (with-stdout-to
    +   example5.output
    +   (run ../analyzer taint example5.ll))))
    +
    +(rule
    + (alias runtest)
    + (action
    +  (diff example5.expected example5.output)))
h2oche commented 3 years ago

Thanks for your clarification.

  1. I asked the first question since I already implemented the analysis without explicitly using meet operator. I just want to know if it is okay. Is it okay to leave "Not implemented"?
  2. I tried to update dune/test as your diff, but I got error. I think there is no example4.expected and example5.expected files in our repository.
KihongHeo commented 3 years ago
  1. It is totally ok to implement filter without explicitly using meet. But I strongly recommend you implement meet since we might have unit tests for some operators, for the grading.

  2. Yes. Thank you again. Here are the files.

new file mode 100644
index 0000000..ac488ee
--- /dev/null
+++ b/test/example4.expected
@@ -0,0 +1 @@
+Potential Tainted-flow @ example4.c:main:5:3 (call void @sink(i32 %call), !dbg !14)
diff --git a/test/example5.expected b/test/example5.expected
new file mode 100644
index 0000000..ccb4aef
--- /dev/null
+++ b/test/example5.expected
@@ -0,0 +1 @@
+Potential Tainted-flow @ example5.c:main:12:3 (call void @sink(i32 %y.0), !dbg !23)
h2oche commented 3 years ago

넵, 한 학기 동안 감사했습니다!