> I'd just like to express my enthusiasm for taking a formal approach to the > kernel language. For everything outside the kernel, defining it by > self-hosting, by a meta-circular interpreter (where the interpreter is > written only in the kernel subset of the language) or by desugaring is fine. > These other techniques may or may not be ideal for expressing the semantics > of these non-kernel constructs, but it does ensure that an adversary's code > cannot take any action beyond those actions allowed by the kernel language.
It's important to distinguish whether this is a valuable exercise for: 1) research; 2) groups focused on security; or 3) the language standard. (I know security is not a separable concern. But it is also not the exclusive concern of language design.) I am thrilled that researchers are working on formal models of ES. But it's not within the purview of TC39 to do research. And there's nothing wrong with an unofficial, non-normative formalization of a normative spec coming out of an entirely different group. It could be just as useful-- and would undoubtedly be of higher quality-- than one we tried to do in the standard. > All security reasoning is reasoning about limits on what an adversary may do. > Thus, all security arguments rest on an induction over all the actions > available to the adversary. This statement's pretty muddled. Your "thus" does not follow (there are more proof techniques on heaven and earth, Horatio...) and your induction is not defined. But I see that Sergio, John, and Ankur have some papers with formal definitions-- I look forward to reading them. Thanks for the links. Dave _______________________________________________ es-discuss mailing list es-discuss@mozilla.org https://mail.mozilla.org/listinfo/es-discuss
