Repository navigation
Expand file tree
/
Copy pathprojects.html
More file actions
65 lines (61 loc) · 8.69 KB
/
Copy pathprojects.html
File metadata and controls
65 lines (61 loc) · 8.69 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
**Verification for Security (XM_0099)**
[*Klaus v. Gleissenthall*](https://gleissen.github.io/)
[Back](index.html)
Project Ideas
==============================================================
- Extend our verifier with pointers and prove the correctness of a pointer manipulating program (say, a linked-list implementation).
- Extend our verifier with Bitvector types. Implement a crypto-algorithm (AES, SHA) and prove its correctness.
- Build a larger verified application with our verifier and add a runtime with webassembly (you can use [this](https://www.wasm.builders/gunjan_0307/compiling-javascript-to-wasm-34lk) as a starting point).
- Add automation to our verifier by implementing [this paper](https://users.soe.ucsc.edu/~cormac/papers/fme01.pdf). This is an easier algorithm than the one discussed in class.
- Implement IFC type system for nano, and write a secure application.
- Implement a program synthesis tool. Take a look at [this blog post](https://barghouthi.github.io/2017/04/24/synthesis-primer/) to get you started. Can you think of a class of programs where sythesis is particularly useful?
- Add Horn clause inference via predicate abstraction to the verifier, as discussed in class.
- Implement this [type system](https://people.eecs.berkeley.edu/~necula/Papers/ccured_toplas.pdf) for memory safety.
- Implement a different type system for memory safety: see [this](https://borretti.me/article/type-systems-memory-safety) for inspiration.
- Extend our verifier to make it more usable. Whenever Z3 produces a counterexample use [QuickCheck](https://hackage.haskell.org/package/QuickCheck) to test if the counterexample is reachable. If yes, the program is incorrect. Else, the invariant has to be refined.
- Add a “decreases” annotation to the verifier, like in [Dafny](http://dafny.org/latest/DafnyRef/DafnyRef#sec-decreases-clause). This can be used to prove termination. Use can use [this](https://ethz.ch/content/dam/ethz/special-interest/infk/chair-program-method/pm/documents/Education/Theses/Patrick_Gruntz_BA_report.pdf) as starting point.
- Implement this optimized [verification condition generation algorithm](https://users.soe.ucsc.edu/~cormac/papers/popl01.pdf).
- Build a VCGen based verifier for LLVM IR, e.g., using [this library](https://hackage.haskell.org/package/llvm-hs).
- Reimplement [this paper](https://files.sri.inf.ethz.ch/website/papers/sigcomm20-netdice.pdf) for probabilistic network verification.
- Reimplement [this paper](https://www.cs.princeton.edu/~dpw/papers/minesweeper-sigcomm17.pdf) for SMT based network verification.
- Reimplement [this algorithm](https://theory.stanford.edu/~arbrad/papers/Understanding_IC3.pdf) for checking program correctness automatically. Can you use it to verify an interesting program?
- Add a more advanced memory model to our verifier. To start, take a look at [this paper](https://link.springer.com/chapter/10.1007/978-3-540-93900-9_24) or [this paper](https://arxiv.org/pdf/1703.00053.pdf).
- Build a VCGen based verifier for Verilog hardware.
- Build a type system checking for memory safety for LLVM, building on [this paper](https://people.eecs.berkeley.edu/~necula/Papers/ccured_toplas.pdf).
- Build an automated verifier e.g., using [liquid fixpoint](https://github.com/ucsd-progsys/liquid-fixpoint), that proves bounds checks for arrays in LLVM IR.
- Implement a staged verifier for C code; see [this paper](https://dl.acm.org/doi/pdf/10.1145/3009837.3009867) for inspiration.
- Typecheck OS code using IFC, see [this paper](http://www.scs.stanford.edu/histar/).
- Build an IFC language and type-system for Verilog, and use it to prove timing-chache side-channel freedom. See also [this paper](https://www.cs.cornell.edu/andru/papers/asplos15/asplos15.pdf).
- Build an automated verifier (e.g., using liquid fixpoint) that verifies leakage freedom for software by building a product program see [this paper](https://www.usenix.org/conference/usenixsecurity16/technical-sessions/presentation/almeida) for inspiration.
- Build a VCGen based verifier for BlueSpec Verilog.
- Implement invariant generation using non-linear solving, following [this paper](https://link.springer.com/chapter/10.1007/978-3-540-45069-6_39).
- Implement [liquid types checking](https://arxiv.org/pdf/2010.07763.pdf).
- We can use arrays to reason about concurrent programs that are run with arbitrary many threads. Each array element is used to encode the local state of one of the threads. See e.g., [this paper](https://dl.acm.org/doi/10.1145/3009837.3009893). Implement and verify a challenging concurrent algorithm.
- Implement an IFC type system for assembly to prove timing-channel freedom.
- Build a verifier that can prove absence of spectre gadgets.
- Build a type-system to protect against a different spectre variant or row-hammer.
- Implment the program transformation (for removing side-channels) from [this paper](https://arxiv.org/abs/2104.10749) and add a type system showing its correctness.
- Implement this [calculus of depenedency](https://dl.acm.org/doi/pdf/10.1145/292540.292555) which generalizes IFC type checking. Can you use it to write secure programs?
- Implement this [type system](https://dl.acm.org/doi/pdf/10.1145/292540.292555) to prove security for effectful programs. Can you use it to prove security of an interesting program?
- (Re-)Implement this [idea](https://www.cs.jhu.edu/~fabian/courses/CS600.624/proof-carrying-code.pdf)--proof carrying code.
- Implement a verifier based on relational Hoare logic (medium), or probabilistic Hoare logic (hard), see these [lecture notes](https://software.imdea.org/~gbarthe/__introrelver.pdf).
- Implement an alternative approach to Horn clause solving e.g., from [this paper](https://arxiv.org/pdf/1610.06768.pdf) or [this paper](https://link.springer.com/chapter/10.1007/978-3-319-08867-9_55).
- Implement a VCGen-based verifier for P4 networking code.
- Implement ideas from [this paper](https://link.springer.com/chapter/10.1007/978-3-642-14295-6_7) to prove program termination or non-termination via ranking functions.
- Implement a verifier for Rust, following [this paper](https://arxiv.org/pdf/2002.09002.pdf).
- Define a semantics and correctness notion for [Hertzbleed](https://www.hertzbleed.com).
- Implement a type checker for masking implementations against power side-channels, see [this paper](https://eprint.iacr.org/2015/506.pdf).
- Implement a checker for differential privacy, see [this paper](https://dl.acm.org/doi/pdf/10.1145/3158146) or [this paper](https://www.cse.psu.edu/~dbz5017/pub/popl17.pdf).
- Extend our verifier with [refinement proofs](https://dl.acm.org/doi/pdf/10.1145/3492545), for security or concurrency. What would be a good way to represent these proofs at the program level?
- Implement a verifier for neural networks: see these [lecture notes](https://verifieddeeplearning.com/nnv_book.pdf).
- Implement [this paper](https://arxiv.org/pdf/1303.2489.pdf) to build an automated verifier that can deal with more complicated data-structures like linked-lists.
- Networks can have side-channels and leak via inter-packet timing. Design a security notion for networks based on differential privacy, see [this paper](https://www.cis.upenn.edu/~sga001/papers/ifs-ccs21.pdf) and [this paper](https://arxiv.org/pdf/1905.02383.pdf).
- Implement an IFC type systen for [Spinal HDL](https://github.com/SpinalHDL/SpinalHDL) and use it to check security properties of [this processor](https://github.com/proteus-core/prospect/tree/master).
- Build an IFC language for software that proves leakage freedom, under a specific hardware contract: see [this paper](https://gleissen.github.io/papers/ccs2023.pdf).
- Build an IFC system that verifies leakage model for Verilog hardware, see [this paper](https://gleissen.github.io/papers/ccs2023.pdf) and [this paper](https://www.usenix.org/system/files/usenixsecurity23-daniel.pdf).
- Build a program semantics for Rowhammer and define a notion of security.
- Verify parts of Rust’s foreign function interface, see [this paper](https://goto.ucsd.edu/~rjhala/hotos-ffi.pdf).
- Implement a type-checker for probabilistic proofs of cryptographic protocols, see [this paper](https://dl.acm.org/doi/pdf/10.1145/3571223).
- Implement a verifier for quantum algorithms, see e.g., [this paper](https://dl.acm.org/doi/10.1145/3582016.3582039).
- Use Farkas’ lemma, see [this paper](https://link.springer.com/chapter/10.1007/978-3-540-45069-6_39) to automatically infer invariants for quantum programs.
<!-- Markdeep: --><style class="fallback">body{visibility:hidden;white-space:pre;font-family:monospace}</style><script src="markdeep.min.js" charset="utf-8"></script><script src="https://morgan3d.github.io/markdeep/latest/markdeep.min.js" charset="utf-8"></script><script>window.alreadyProcessedMarkdeep||(document.body.style.visibility="visible")</script>