Thesis Sketch

This is very rough sketch of what I expect the thesis to look like.

Introduction

Some fluffy motivation. Malware is common-place. So is vulnerable software. Imagine that we could be without it.

Define proof-carrying code, and why it could potentially solve the problem. Talk about its history and pitfalls.

Introduce the concept of TAL. Talk about previous problems (forced garbage collection, lack of control).

Introduce Rust, lifetimes, borrow checking.

We are now ready to introduce the subject of the thesis: Will it blend?

Rust TAL

Define the language, including the type system. Give an intuition about why it works. Postulate soundness/safety.

Implementation

Introduce my implementation. The current plan is:

• Write programs that can be assembled using nasm. Include annotations in comments.

• Have a python script for rewriting the assembler to valid Agda.

• Have a type-checker written in Agda along with a soundness proof.

Building stuff

Depending on the direction the thesis goes, this chapter might be expanded.

The minimal viable version includes a semi-handwavy description of how one can use the primitives postulated in the previous chapter to build a useful sandbox.

A more expanded version would include a examples of my implementation doing (very small-scale) useful stuff.

Proof of soundness

This chapter would include a human-version of proof of soundness. The machine-verifiable version is in the appendix.

Ideally the human-version would not simply be a transcription of the machine-version, but would actually give some intuition into the proof.

Evaluation

Though I will be sure to introduce the assumptions of my design as it is introduced, some of the implications of these choices might not be immediately obvious (especially the negative ones).

This chapter would include an evaluation of the method developed in the paper. This would probably include:

• The implementation is obviously not very usable in practice. Why not?

• What features are missing? How many of those simply require more work, and how many need non-trivial design extensions?

• Assume that all the trivial extensions were fulfilled. Would the implementation then actually be useful?

Future work/Related work/Conclusion

Some stuff.