prosyslab-classroom / is661-advanced-software-security Goto Github PK

Homework 3 is to review the papers of other students.
Each student has two papers to review.
Read the assigned papers carefully and write reviews in detail.

Requirements

• English
• more than 700 words
• Sample review: http://ezyang.com/reviews/pldi14-rlimits.txt

Due date

Due: 3. 21. (Thur.) 23:59:59

Hi, everyone.

This is the announcement for Homework 2.
Read the instruction HW2: Your quick sort paper and write a paper.

Here is the GitHub classroom link for this homework:
https://classroom.github.com/a/6Uoc2spX

You MUST submit both:

• commit & push your tex & pdf files to your homework repository,
• and submit your pdf file to the HotCRP.

Use the "New HW2 submission" button on the HotCRP.

Don't assign any conflict.

Syntactic Requirements (Different from the template README.md)

• You can write more than 2 pages, but only up to 5 pages. More pages for references (bib) are permitted.
• Write your paper in the structure of general technical papers including abstract, introduction, etc.
• Write in English (한국인 학생들도 영어로 작성하세요). Your paper will be reviewed by other students (HW3).

Due date

Due: 3. 12 (Tue.) 23:59:59 --> 3. 13 (Wed.) 05:59:59

Here is the invitation link for the homework:

• Homework 4: https://classroom.github.com/a/Xyn1Z3kz (due: 23:59:59, Apr. 28)

One shall implement a program verifier that automatically checks non-trivial semantic properties with z3 by extracting CHC formulae.

Hi all,

I rescheduled the midterm presentation plan since we have a number of students. The new schedule is as follows (sorry if your English name is wrong):

• Apr. 14 (Thr), 09:00 - 10:15 : 이강욱 (Kangwook), 김태은 (Taeeun), 이해인 (Haein)
• Apr. 19 (Tue), 09:00 - 12:00 : 이강욱 (Kangwook), 정원영 (Wonyoung), 안해찬 (Haechan), 이시훈 (Sihoon), 권승완 (Seungwan), 김영훈 (Younghun)
• Apr. 26 (Tue), 09:00 - 10:15: 박종찬 (Jongchan), 박준영 (Joonyoung), 백민우 (Minwoo)
• Apr. 28 (Thr), 09:00 - 10:15: 백민우 (Minwoo), 장수진 (Sujin), 최재호 (Jaeho), Jonas Brager Jacobsen

Hope we have interesting discussions.

Hi, I'd like to ask a question about Alive2(승완's presented paper).

The simple translation example you mentioned is following:

foo (int x):
  y = x + 0
  ret y

=>

foo (int x):
  y = x
  ret y

In this example,
How does the refinement([[T]] <= [[S]]) check works?
What is the abstract value of y?
How is the abstract semantics of + defined?

Thanks.

Hi,

Our final project will consist of the following steps which will be the same as typical academic publication processes:

1. Write a proposal: You will write a research proposal for your final project. Create an account for the submission site using your own name and KAIST email. Maximum 2 pages in English. The GH invitation link will be provided soon. Proposal submission deadline: Apr 29 23:59:59 (strict)

2. Give a lightning talk: You will give a lightning talk (5 min, up to 3-page slides) on May 3.

3. Write reviews for proposals from other students. Each of you will get 3 proposals.

4. Submit your final project code: Our TA will give you GH invitation link later. Deadline: May 24

5. Give a presentation.

During the semester, one shall encounter a few programming assignments.

Each assignment requires you to write a program in OCaml.

It needs a bit of environment setup, which may be frustrating if you are new to OCaml.

In order to help you focus on implementing the core logic of each assignment, we provide pre-built docker image and KCLOUD VM.

For your information, please follow the instructions from the slides.

Hi.

1. No class next Tue (May 17)
2. See the updated presentation schedule: #17

• 15 min including QnA (strict)
• send your slides to TAs before the class

Hello, I'm Yeonghun and this issue is the responses for the questions I got in the presentation.

First, the professor's question was,

"Why are the testcases said to be verified even if they have non-zero alarms?"

The verified check mark does not mean that a testcase is bug-free, but it means that a verifier(e.g., VERISMART) can pinpoint all vulnerable locations in the sourcecode.

and for the Taeeun's second question,

"Why did Zeus fail to verify all testcases even the testcases are the ones in its paper?"

To put it briefly, a verifier is said to fail to verify a testcase if it has any false positives.

I'll quote the explanation in the paper as follows,

However, the public data was not detailed enough to accurately interprete as the ZEUS authors classify each benchmark contract simply as ‘safe’ or ‘unsafe’ without specific alarm information such as line numbers. The only objective information we could obtain from the data [28] was the fact that ZEUS produces some (nonzero) number of false (arithmetic-overflow) alarms on 40 contracts, and we decided to use those in our evaluation.
...
The column
Verified indicates whether each tool detected all bugs without
false positives (✓: success, ✗: failure).

Thank you for the questions!

Hi, all

Your submissions have been reviewed and 3 students got desk reject.
I have sent an email to students who got desk reject.

Dear students who got the desk reject mail,
Check the email, and resubmit your updated paper by 12 p.m. Today
You will get 70% of total score for this homework if you resubmit,
Otherwise you will get 0 point.

Here are the invitation links for homeworks:

• Homework 0: https://classroom.github.com/a/Y5hLY6J9 (due: none)
• Homework 1: https://classroom.github.com/a/mvRrBqG5 (due: 23:59:59, Mar. 11)

There is no deadline for homework 0. We will not grade the homework, thus no penalty at all.
Still, we highly recommend doing the homework, if you are not familiar with OCaml, git or GitHub.

For homework 1, you shall submit a reading critique for the article published in WIRED 2021.

Hello, I'm Jaeho Choi (20223684).

I noticed that my proposal is ill-formed. I just realized that there is a specified format for the proposal.
Should I rewrite the proposal and submit it?

Sorry for the inconvenience.

Hi,

The "test 2" of satTest.ml can fail even if sat.ml has been correctly implemented.
It expects (SAT (false, false, false)) as the return value for solve (And (Or (Z, Not Y), Or (Not X, Not Z))).
However, since (SAT (true, false, false)) is also a satisfying assignment for the given formula, the test is not correct.
I think it should be fixed to allow any satisfying assignments for given formula since there was no specification of this issue in the problem description.

Thanks.

Here is the invitation link for the midterm project:

• Midterm: https://classroom.github.com/a/qONiCsu_ (due: see attached docs)

One shall implement a program synthesizer that automatically generates SmaLLVM programs from given input-output examples.
The detailed policy and schedules regarding the project are further described in this document.

Here are the grading criteria for the upcoming midterm presentations (see #13 for the schedule).

1. Novelty of the idea (아이디어 독창성)
2. Presentation delivery (발표 전달력)
3. Questions and answers (질의응답)

We will grade each item from zero to five (0-5).

Here is the invitation link for the homework:

• Homework 2: https://classroom.github.com/a/Kd6ckhI0 (due: 23:59:59, Mar. 22)

One shall submit a reading critique for the article published in CACM 2018.
For submission, please find the Reading Critique 2 slot in Gradescope and submit a pdf file.

According to this document, the midterm project has two due dates(April 1st and 4th).

Will the grade for already-provided test cases be detertmined at first due date or second due date(altogether with student-provided test cases)?

Thanks.

Hi all, here are the guidelines for our final project.

1. Proposal and lightning talk (30%)

• Problem: what your problem is. why it is important. show real examples.
• Novelty: how novel your solution is. why it works. show why existing works do not work.
• Practical impact: how your approach is. show your expectation.
• Presentation quality: how clear your presentation is.

2. Review (30%)

• Understanding
• Questions
• Suggestions

3. Final presentation (30%)

• Completeness: achievement with respect to the original plan
• Critical thinking: analysis of your successes and failures
• Presentation quality
• QnA

4. Participation (10%)
   Questions and comments during lightning and main talks.

Hi,

Many of your critiques are very interesting and well-written. I enjoy reading your writings. Especially, I want to share three good writings by

• Taeeun Kim
• Seungwan Kwon
• Haechan An

I recommend you read their articles.

I only submitted my pdf file to Gradescope, not pushed it into my github repository.

Is it okay?

Hi all,

There will be no class on May 10 because our TA, Hyunsu, and I will present a paper at ICSE next Tue 9 am.

Each student presentation will be pushed back and resume next Thursday. See the schedule table.

For korean students, is it necessary to write a proposal in korean?

Hi, everyone
This is the announcement for final project presentation.
Prepare a 25-minute presentation according to the following schedule table.

Requirements:

• 30 minutes (25 minutes for presentation + 5 minutes for Q&A)
• English
• Submit your presentation slide by 6 p.m. the day before the presentation to email: [email protected]
• Follow the presentation format:
  • motivation
  • problem
  • idea + killer example + appealing result
  • technical details
  • evaluation
  • conclusion
• Present the final version of your project

Hi all,

I fixed a typo in the lecture slide (lecture10.pdf, page 19), and updated the example (lecture10.pdf, page 20).

Let me summarize the discussion about the freshness from today's lecture.

1. What does freshness mean?
   Independently pick up a new value without making unnecessary relationships with existing values.

2. What happens if we don't have the freshness restriction?
   The proof system becomes unsound. That means you can prove a false formula (see the new example).

Hope this clarifies all things.

Hi, everyone.

This is the announcement for Homework 4 and Final project.
Read Project Theme: Understandable & Explainable Programming Systems and prepare your final project.

Homework 4: Project proposal

• GitHub classroom link: https://classroom.github.com/a/Z8RmXu9I
• Use the "New HW4 submission" button on the HotCRP.
  
• Due: 4/2 23:59:59

You will present your project proposal according to the schedule announced in #40 .

Final: Project paper

• GitHub classroom link: https://classroom.github.com/a/1Hym3jbh
• Use the "Final submission" button on the HotCRP.
  
• Due: 6/11 6/1 6/5 23:59:59

The schedule for the final project presentation will be announced later.
(update) You will present your final project according to the schedule in #49

Submission guide

You MUST submit both:

• commit & push your tex & pdf files to your homework repository,
• and submit your pdf file to the HotCRP.

Don't assign any conflict.

Syntactic Requirements (Different from the template README.md)

• You can write more than 2 pages, but only up to 10 pages. More pages for references (bib) are permitted.
• Write your proposal and paper in the structure of general technical papers including abstract, introduction, etc.
• Write in English (한국인 학생들도 영어로 작성하세요). Your proposal will be reviewed by other students (HW5).

Hi all,
Homework 3 is graded. You can check your score at KLMS.
Reviews with less than 700 words have been deducted.
If you have any question, send an email [email protected].

Hi all,
Homework 1 is graded. You can check your score at KLMS.
If you have any question, send an email [email protected].

Hi all,
The due date for the final project paper has been moved up to June 1st
Please check the course schedule and final project presentation schedule #49.

Homework 5 is to review the published papers.
Each student has two papers to review.
Read the assigned papers carefully and write reviews in detail.

Requirements

• English
• More than 700 words per review
• Sample review: http://ezyang.com/reviews/pldi14-rlimits.txt

Due date

Due: 5. 14. (Tue.) 23:59:59

In test/verifier.h, the assume function is declared as void assume(int).
Since it is not declared with void assume(bool),
we can write program such as

#include "verifier.h"
int main(){
  int x = input();
  assume(x);
  assert(x!=0);
  return 0;
}

Should we consider the above case, too?
Or can we safely assume that the expression inside assume is limited to boolean expressions.

Thanks.

Hi,

Since the paper presentation schedule has been delayed, we decided to postpone the deadline for submitting the final project code.

The changed deadline is May 30th, 11:59 pm.

Thanks.

Hi, everyone
This is the announcement for paper presentation.

Each student will present two papers.
Prepare a 15-minute presentation for each paper according to the following schedule table.

Requirements:

• 18 minutes (15 minutes for presentation + 3 minutes for Q&A)
• English
• Submit your presentation slide by 6 p.m. the day before the presentation to email: [email protected]

Hi all,
Homework 2 is graded. You can check your score at KLMS.
If you have any question, send an email [email protected].

Hi, everyone
This is the announcement for paper presentation.
Each student will present two papers after the midterm period, 4/23 ~ 5/14 (as in the course schedule).
Submit your preference to the following survey, then we will assign you two papers.
https://forms.gle/2e2UcFEBbisGCpc86

Due: 3. 6. (Wed.) 23:59:59

Hi all.

I have read the papers submitted so far.
Unfortunately, it is hard to believe you have watched the video. Many tips introduced in the videos are ignored.

I will give you 6 more hours.
If you want to improve your submission, try your best and show that you are an eligible KAIST grad student.
Read the papers of your advisor and follow the format, outlines, etc.

Hi all,

Please submit your homework 1 to Gradescope. Only 12/14 have been submitted so far.

Sorry for the confusion. Next time, we will clarify the submission process.

Here is the invitation link for the homework:

• Homework 3: https://classroom.github.com/a/yVTu6_Zv (due: 23:59:59, Apr. 14)

One shall submit a reading critique for the article published in CACM 2021.
For submission, please find the Reading Critique 3 slot in Gradescope and submit a pdf file.

As notified in the class, we will throw a pizza party for lunch after the midterm presentations (Apr. 19). RSVP to the poll to figure out the pizza demands:

• Pizza party poll: https://forms.gle/4eyjQBcsgKKecw7M7 (due: 23:59:59, Apr. 7)

1. Depending on your implementation, the counter-example may be different from *.expected, as pointed out in #21. We are aware of the issue and will consider it when grading.
2. For the submission of homework 4, push your implementation to master branch in GitHub repo.

Hi, everyone
This is the announcement for research talk and project proposal talk

Each student will present two talks: research talk on your quicksort paper and project proposal talk.
Prepare a 15-minute presentation for each talk according to the following schedule table.

Requirements:

• 18 minutes (15 minutes for presentation + 3 minutes for Q&A)
• English
• Submit your presentation slide by 6 p.m. the day before the presentation to email: [email protected]
• Follow the presentation format:
  • motivation
  • problem
  • idea + killer example + appealing result
  • technical details
  • evaluation
  • conclusion

Hi, everyone.

Here are some things you should set up for this course.

• Submit your GitHub account: https://forms.gle/nD1Aair2zftpcwEMA
• Join the HotCRP: https://kaist-asos2024.hotcrp.com

Homework 1

Homework 1 is to write an essay.
Read the article on the first week of schedule table and write a critique.
Here is the GitHub classroom link for this homework:
https://classroom.github.com/a/URSlawq_

Push your essay to your homework repository, and submit your pdf file to the HotCRP.
Use the “New HW1 submission” button.

Due date

Due: 3. 3 (Sun.) 23:59:59

Hi all,
Research Talk is graded. You can check your score at KLMS.
If you have any question, send an email [email protected].

In HW4, my implementation failed in test/example4 with these diff log:

                     (E Int)
                     (F Int)
                     (G Int)
-                    (H Int)
-                    (I Bool))
-             (! (=> (and (while.end G C I H E B A D F) (not (>= E 0)))
-                    (if.else false G C I H E B A D F))
+                    (H Bool)
+                    (I Int))
+             (! (=> (and (while.end C A B E F H D I G) (not (>= F 0)))
+                    (if.else false C A B E F H D I G))

I think it's just a difference in the names of the variables, so is it okay to ignore this log?

Thanks!

Here is a good introductory video of Godel's incompleteness theorem.
In the field of programming languages, logic, program analysis, etc, you will directly or indirectly encounter this problem many times in the future. All the following are actually related to the theorem:

• Turing's halting problem
• Why sound and complete program analysis is impossible
• Why inductive loop invariant is important (we will discuss this in the next lecture or later)

I encourage everyone to watch this video: https://www.youtube.com/watch?v=I4pQbo5MQOs

In the 10-12th week, each student will present a paper about program synthesis or program verification.
To assign papers, submit your preference to the following survey:

• https://forms.gle/brgu3wWCbkpQydaN6 (due: Thursday, April 7th, 23:59)

Hi,

Our review process gets started!

• Each of you is assigned to review two papers.
• Each proposal will have 3 or 4 reviews.
• Review due on May 11, 23:59:59
• Rebuttal due on May 13, 23:59:59

Here is the invitation link for the final project:

• Final: https://classroom.github.com/a/zOSv-HdM

Please refer to #14 for the rubric and schedule.

Schedule

Each student will present for 20 minutes and answer for 5 minutes.
The schedule is as follows (only includes those who submitted the proposal) :

5.31(Tue): Younghun Kim, Jongchan Park, Sujin Jang
6.2(Thr): Haein Lee, Wonyoung Jung, Kangwook Lee
6.7(Tue): Jooeyoung Park, Seungwan Kwon, Haechan An
6.9(Thr): Sihoon Lee, Jaeho Choi, Taeeun Kim

Criteria

Check this announcement: #19
And also, note that you can present in Korean.

Pizza Party Pole

As notified in the class, we will throw a pizza party for lunch after the final presentations (June. 9). RSVP to the poll to figure out the pizza demands:

• https://forms.gle/4eyjQBcsgKKecw7M7 (due: 23:59:59, June. 8)

Hi,

I'd like to ask which subset of LLVM instructions should we consider to exist in the input programs.
In the provided examples(example1.ll to example5.ll),
the kind of instructions are limited to the followings:

      | Llvm.Opcode.Br 
      | Llvm.Opcode.Call
      | Llvm.Opcode.ICmp
      | Llvm.Opcode.ZExt
      | Llvm.Opcode.PHI 
      | Llvm.Opcode.Add
      | Llvm.Opcode.Ret

Can I only consider those instructions?

Thank you.

#Here is the result of the paper assignment, grading criteria, and the schedule.

Paper Assignment

We assign the paper for each student using the DragonBall Z3. Those who didn't submit their preferences have been assigned to a randomly selected paper.

Here is the result:

• Seungwan Kwon: Alive2: bounded translation validation for LLVM, PLDI'21
• Younghun Kim: VERISMART: A Highly Precise Safety Verifier for Ethereum Smart Contracts, SNP'20
• Sujin Jang: Verifying Correct Usage of Context-Free API Protocols, POPL'19
• Joonyoung Park: Towards a Verified Range Analysis for JavaScript JITs, PLDI'20
• Kangwook Lee: Combinatorial sketching for finite programs, ASPLOS'06
• Jonas Brager Jacobsen: Synthesis of Data Completion Scripts using Finite Tree Automata, OOPSLA'17
• Haechan An: Reluplex: An efficient SMT solver for verifying deep neural networks, CAV'17
• Sihoon Lee: Syntia: Synthesizing the Semantics of Obfuscated Code, USENIXSEC'17
• Haein Lee: Verifying Constant-Time Implementations, USENIXSEC'16
• Jongchan Park: Verified Three-Way Program Merge, OOPSLA'18
• Taeeun Kim: Synthesizing Highly Expressive SQL Queries from Input-Output Examples, PLDI'17
• Wonyoung Jung: Optimizing Homomorphic Evaluation Circuits by Program Synthesis and Term Rewriting, PLDI'20
• Jaeho Choi: Data-Driven Synthesis of Provably Sound Side Channel Analyses, ICSE'21
• Minwoo Baek: An Inductive Synthesis Framework for Verifiable Reinforcement Learning, PLDI'19

Schedule

Each student will present and answer the questions for 15 minutes.
The schedule is as follows (updated):

• 5.19 (Thr): Seungwan Kwon, Sujin Jang, Sihoon Lee, Younghun Kim
• 5.24 (Tue): Taeeun Kim, Jaeho Choi, Haein Lee, Jongchan Park, Minwoo Baek
• 5.26 (Thr): Joonyoung Park, Kangwook Lee, Haechan An, Wonyoung Jung, Jonas Brager Jacobsen

Criteria

The grading criteria for presentations are as follow:

1. Understanding of the paper (내용에 대한 이해)
2. Presentation Delivery (발표 전달력)
3. Critical Thinking (비판적 사고)
4. QnA (질의 응답)

We will grade each item from zero to five (0-5).

When counterexamples are detected in the target code, it was mentioned that the SMT solver checks whether this counterexample is fake or not. To me, this seems to imply that SMT solver can provide the ground truth of the given target code's validity. Then why not just use SMT solver to verify the target code?