CS 260r 2017 L5: Jitk: A Trustworthy In-Kernel Interpreter Infrastructure (2/5)
Jitk security filters are defined in SCPL, a new language, but the kernel verifier—the most important contribution—accepts BPF filters as input. SCPL requires an additional proof layer, a burden. What is an advantage of SCPL?
The last paragraph of §5.3 seems very precisely worded. When the authors say Lemma 3 “provides a strong sanity check on the internal consistency of our encoder and decoder,” is this simply another way of saying Lemma 3 proves the correctness of their encoder and decoder? Why or why not?
Never submit passwords through Google Forms.
This form was created inside of Google Apps for Harvard.
Terms of Service