- Due 4/17
- JIT-ROP. Traditional ROP attacks can be executed in a one-shot manner against a target machine. How does JIT-ROP's attack model differ? Could a JIT-ROP attack be carried out if the attacker does not have the capability to execute arbitrary (JavaScript) code on the target machine?
- Shuffler. Shuffler runs at the same level of privilege as the code it defends. What measures does it take to ensure the security of its own code? Do any potential attacks against Shuffler itself remain? What would be the advantages and disadvantages of performing shuffling from the OS kernel?
- Due 4/10
- Adversarial learning. The world increasingly relies on machine learning systems, yet they are vulnerable to all sorts of security, correctness, and understanding issues. Do you think 10 years from now machine learning will replace a lot of human decision making, or do you think that it will be used in only limited domains? Explain your answer.
- Unlearning. How would you apply the unlearning approach to Neural Networks?
- Due 4/3
- AppInsight. If the dependency graph AppInsight collects is incomplete (e.g., the graph misses certain edges), what problems may occur? How would you go about fixing the problems?
- AppDoctor. How would you augment AppDoctor to crawl app UI more effectively?
- Due 3/27
- NEZHA. What are the advantages and limitations of symbolic execution in the context of fuzzing?
- angr. Write a useful analysis using angr and run it on some binaries.
- Due 3/20
- Magpie. Mac users occasionally suffer from the "spinning beach ball" problem when their applications hang and the Mac OS displays a spinning beach ball. Would the Magpie idea help diagnose this problem? If so, explain how; otherwise, explain why it won't help.
- Modist The Chess system uses preemption bounding to search the state space of multithreaded programs. What's the equivalent of context bounding in model-checking distributed systems?
- Due 3/6
- Hybrid Race Detector. Construct a code example with fewer than 50 lines that shows that the Oversized Lock Condition reduces the number of events to track.
- Parrot. Construct a code example with fewer than 50 lines that runs very slowly with Parrot on some inputs regardless of what performance hints one inserts.
- Due 2/27
- Delta debugging. Outline how you would apply delta debugging on data races (concurrent accesses to the same shared memory location with at least one write) to isolate the thread schedules that trigger the races. Assume you have full control over the thread scheduler and can generate whatever thread schedules you want.
- Rx. Explain how you would apply the Rx idea to recover from stack buffer overflows.
- Due 2/20
- Verdi. Based on your understanding of the paper, model the network semantics where a set of "malicious" nodes can send arbitrary messages.
- Ironfleet. Try to use Dafny to reason about
the pigeonhole principle.
As a reference, you may use the following prototype form:
lemma lemma_set_Pigeonhole_Principle_On_Subsets(s : set<int>, a : set<int>, b : set<int>) requires a <= s && b <= s requires |a| + |b| > |s| ensures exists x :: x in a && x in b { // Fill the proof here. }
- Due 2/13
- Meta-compilation. Based on your understanding of the paper, write a checker that finds memory leaks.
- EXE. Construct a worst case example to make the array-based refinement algorithm add n(n-1)/2 array axioms. State the assumptions you make.
- Due 2/6
- Chess. Chess enforces single-threaded executions to target systems. Explain what would be challenges if we use multi-threaded executions there.
- DPOR. In the algorithm shown in figure 3, DPOR would explore all enabled transitions of a state in the fallback case (as in line 7). Provide an example that triggers this case.
- Due 1/30
- Memcheck. Would valgrind detect the buffer overrun in the following code? Why or why not?
int foo(void) { int a[2] = {0}; a[2] = 10; // off by 1 } - Baggy bounds check. Suppose slot_size is set to
16 bytes. Consider the following code snippet:
char *p = malloc(256); char *q = p + 256; char ch = *q;Explain whether or not baggy bounds checking will raise an exception at the dereference of q.
- Due 1/23
- Detours. Given a code location to insert a probe, Detours writes a jump instruction at this location. What may go wrong and how can you fix these issues?
- Pin. Write a Pin module that replaces malloc() calls with my_malloc() calls. You can get Pin from here.