is661-advanced-software-security's People
Forkers
arranstewart-dev duncan020313 yeonhee-ryou leehahoon re-st fraglantia jidoc01 doit-man topcueis661-advanced-software-security's Issues
[Announcement] Homework 2 is graded
Hi all,
Homework 2 is graded. You can check your score at KLMS.
If you have any question, send an email [email protected].
[Question][Midterm Project] Due date for grading
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.
[Question][Paper presentation] Alive2 : domain of values
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.
[Announcement] Paper presentation schedule (Updated: 3/14)
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]
[Announcement] Postpone the deadline for submitting the final project code
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.
[Question][Final] Ill-formed final proposal
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.
[Announcement] Hw2
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.
[Announcement] Final project evaluation criteria
Hi all, here are the guidelines for our final project.
- 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.
- Review (30%)
- Understanding
- Questions
- Suggestions
- Final presentation (30%)
- Completeness: achievement with respect to the original plan
- Critical thinking: analysis of your successes and failures
- Presentation quality
- QnA
- Participation (10%)
Questions and comments during lightning and main talks.
[Question][Hw4] Can I ignore variable renaming?
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!
[Announcement] Homework 4 grading and submission
- 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. - For the submission of homework 4, push your implementation to
master
branch in GitHub repo.
[Announcement] Final project presentation schedule
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
[Announcement] submission
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.
[Announcement] Final project due date has been changed: 6/11 -> 6/1
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.
[Announcement] Midterm presentation schedule
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.
[Question][Hw4] Allowed instructions in the input programs
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.
[Announcement] Paper Bidding for Presentation
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)
[Announcement] Homework 5 is out
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
[Announcement] Homework 4 & Final project (Due date: 6/5)
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/116/16/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).
[Question][Paper presentation]Responses for the questions
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!
[Announcement] Homework 4 is out
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.
[Announcement] Scheduling paper presentation (Due: 3. 6. Wed.)
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
[Question][Final Project] Proposal in korean
For korean students, is it necessary to write a proposal in korean?
[Announcement] Final project schedule
Hi,
Our final project will consist of the following steps which will be the same as typical academic publication processes:
-
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)
-
Give a lightning talk: You will give a lightning talk (5 min, up to 3-page slides) on May 3.
-
Write reviews for proposals from other students. Each of you will get 3 proposals.
-
Submit your final project code: Our TA will give you GH invitation link later. Deadline: May 24
-
Give a presentation.
[Question] To paper presentation on [Verifying Correct Usage of Context-Free API Protocols, POPL'19]
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?
[Announcement] No class on May 10
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.
[Question][Hw4] Allowed expression inside `assume` function
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.
[Announcement] Hall of fame
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
I recommend you read their articles.
[Question][Hw0] correctness of test in `satTest.ml`
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.
[Announcement] Homework 2 Desk Reject
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.
[Announcement] Homework 1 is graded
Hi all,
Homework 1 is graded. You can check your score at KLMS.
If you have any question, send an email [email protected].
[Announcement] Homework 3 is graded
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].
[Announcement] Homework 3 is out
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
[Announcement] Paper presentation
#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:
- Understanding of the paper (내용에 대한 이해)
- Presentation Delivery (발표 전달력)
- Critical Thinking (비판적 사고)
- QnA (질의 응답)
We will grade each item from zero to five (0-5).
[Announcement] Midterm project is out
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.
[Announcement] Homework 2 is out (Updated: 3/12)
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
[Announcement] Homework 2 is out
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.
[Announcement] truth != provable
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
[Announcement] Homework 0 and 1 are out
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.
[Question][Hw1] About Submission
I only submitted my pdf file to Gradescope, not pushed it into my github repository.
Is it okay?
[Announcement] Review process starts
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
[Announcement] Schedule
Hi.
- No class next Tue (May 17)
- See the updated presentation schedule: #17
- 15 min including QnA (strict)
- send your slides to TAs before the class
[Announcement] Homework 3 is out (+ pizza party poll)
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)
[Announcement] Environment setup for programming assignments
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.
[Announcement] Research Talk is graded
Hi all,
Research Talk is graded. You can check your score at KLMS.
If you have any question, send an email [email protected].
[Announcement] Final project presentation (+ pizza party pole)
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)
[Announcement] Midterm presentation criteria for grading
Here are the grading criteria for the upcoming midterm presentations (see #13 for the schedule).
- Novelty of the idea (아이디어 독창성)
- Presentation delivery (발표 전달력)
- Questions and answers (질의응답)
We will grade each item from zero to five (0-5).
[Announcement] Research Talk & Project Proposal Talk schedule
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
[Announcement] Final project is out
Here is the invitation link for the final project:
Please refer to #14 for the rubric and schedule.
[Announcement] today's lecture slides
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.
-
What does freshness mean?
Independently pick up a new value without making unnecessary relationships with existing values. -
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.
[Announcement] Setup & Homework 1
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
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.