3 ms·

why ITS was an excellent design vs UNIX Well, first refer to the first Worse is Better essay, which directly compares The Right Thing/MIT vs. Worse is Better/N

by hga 11y ago

why ITS was an excellent design vs UNIX Well, first refer to the first Worse is Better essay, which directly compares The Right Thing/MIT vs. Worse is Better/New Jersey styles in handling of interruption of long system calls (invisible PCLUSER back out vs. return with error and require you to try again: https://www.dreamsongs.com/RiseOfWorseIsBetter.html https://www.dreamsongs.com/RiseOfWorseIsBetter.html). For a few details, the security model was very well matched to the threat model (although they were forced to add login password protection :-), and while constrained in a whole bunch of weird ways, e.g. the 3 local filename components were limited to 6 6 bit-characters, one 36 bit word, total number of directories were the number of words that would fit on a page, 512 I think, it had all sorts of features I miss. E.g. plugable I/O filter and error mechanisms, a [machine-name]: convention, e.g. "AI:DIR;FNAME1 FNAME2" which I think worked on all file accesses, or the general ecosystem's Chaosnet convention of string character ports. And then there's a feature ported to UNIX by Jim Kulp, a hacker with a foot in both worlds, shell job control (^Z and friends). And on MIT-MC, a ECL KL-10 (~2xVAX 11/780), it was seriously fast. I never learned the guts of this (doomed) architecture, but the results spoke for themselves, and exceeded any PDP-10/Decsystem 20 OS I know about. At the highest level, ITS+TECO EMACS+Maclisp was the prototype for the Lisp Machine. As for the ML language family, I'm going for the original formula first, because of all the research I want to be able to better follow that uses it, an allergy to objects I've developed ^_^, and the TCB issue, e.g. the active CakeML project: https://cakeml.org/ https://cakeml.org/ I gather that pretty much anything Magnus Myreen is or has worked on is worth looking at, e.g. he's the guy who solved the seL4 HOL -> CompCert impedance mismatch by going backwards, from GCC produced binary to auto-generated models of what that binary did. If I like ML, I'm sure I'll learn Ocaml, if not, Myreen helped develop a down to the machine code validated LISP for some ACL2 related work: http://www.cl.cam.ac.uk/~mom22/jitawa/ http://www.cl.cam.ac.uk/~mom22/jitawa/ Exactly what I do depends on whether I can grok HOL/this style of proving, haven't done that sort of thing since 1977.... Me-> "a modern web browser is a non-negotiable for users" Maybe. If you want to develop an end user OS that lots of people will use, that might develop a big enough developer community to survive, and that will of course address that very big pain point, well, those are all goals I hold and that I can to contribute to, one way or another. And your exception of "Lots of large companies get by forcing use of terminals, client-server, and minimalist web stuff." doesn't work for the knowledge workers that require access to the unconstrained web. That's so critical nowadays that the PRC still allows it (all but North Korea?), a ticketed programmer friend of mine does his day to day work with access to the web, starting in 1996 I would never accept a programming job that didn't give me such access, etc. etc. The ability to quickly find an answer (if it exists :-) to most any question you can ask from anywhere in the world is just too critical. Hmmm, come to think of it, I'm not exactly enthused by the prospect of trying to run Gnu EMACS on a "secure"/validated system (and I know the C code very well, worked on the parent it forked on for a couple of years. Which just happens to be James Gosling's first C code base with a bytecode interpreter :-). One additional comment on "Worse is Better": Java is an unique? modern example of a "Right Way" system winning, so the "why" would be worth looking at. Ditto the story of Clojure's success, built on top of the JVM. And, yeah, WRT to what seL4 provides, 9,000 lines of code, a fair number of them due to oddities of the hand translation from Haskell to C, isn't going to do much for you, I know it's just the start. But a porting project, and then getting it to do something (blink lights via GPIO or whatever) is for me a good way to start working my way up the stack, learn ARM, etc. Thanks a lot for this discussion and giving me hope WRT to intermediate ways to address the web browser problem!

nickpsecurity 11y ago
It's funny you mentioned the PC losering problem because he countered his own claim later (see p3): https://www.dreamsongs.com/Files/worse-is-worse.pdf https://www.dreamsongs.com/Files/worse-is-worse.pdf The other stuff you mention are good for the time. Extra props for getting work done in direction of LISP machines. I could see that I'd have enjoyed using that system besides the odd quirks you mentioned. Plus, the name of the network is way cooler than the other guys'. ;) re Magnus/ML. I had CakeML in my collection but didn't know about Jitawa + Milawa. I remember skipping it seeing "verified lisp" in abstract while rushing through ACM/IEEE stuff and thinking "I already have VLISP so who cares." However, I appreciate your link because Milawa was a great find: an answer to the "Do you trust the prover?" question that people keep asking. Plus, Jitawa verifying a LISP and it were a nice combo. Knew Magnus was smart but that's extra smart. Anyway, looking at your update, I see CakeML now has a verified compiler and other cool stuff. I might stop recommending FLINT except for diversity. CakeML seems to be the one to build on with VeriML too limited imho: a portable compiler & runtime is always better than an interpreter for Getting Shit Done (TM). So, I appreciate that link. Your HOL work might be tricky. I'll be interested in hearing your experience later as it will inform how other software/systems people might fare. If it's difficult or even before you start, you might want to check out Chlipala's methodology here: http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/ It's more like the FLINT style than HOL. He's produced many solid works with that. His site (link on top) also has interesting tools for various use cases: Bedrock (verified assembly), Ur/Web (correct-by-construction web apps), contribute to Ynot (writing/verifying imperative code), and so on. What they built with it is obvious from descriptions. Their pace has been faster than full verification groups while knocking out lots of errors. There's also more investment of academic brains into Coq theorem prover so each work might benefit from others. Now, a link to help you with what you're actually doing. The seL4 work at some point referenced this book on using Isabelle/HOL for verification. Might be what you need to learn it all. I'd try it first. Stay on it if you're able to do real stuff w/ projects you referenced. Otherwise, backtrack to try Chlipala's methods. http://concrete-semantics.org/ http://concrete-semantics.org/ re browsers. Yes, they're critical for reasons you mentioned. There's a simple solution, though, which I used for years: physical separation w/ KVM switches and guards for information sharing. The browser stuff runs in a PC that handles it. Most of key work or trusted data on other system. The content is translated to formats that make verification easier or at least where you have trusted programs. The guard mediates flow of data to ensure files move back and forth without attacks on memory or transport. It's built as strong you can make it. KVM and drag-n-drop software make it easier to use. Tenix's Interactive Link is an implementation that's very similar. re Worse is Better & Java. I semi-agree. Java is a horrid platform that was successful for these reasons: (a) similarity to existing, mainstream languages, (b) tooling in form of IDE's + libraries, (c) perceived advantages, and mainly (d) massive money in marketing by huge, enterprise firm. So, the strategy worked. Google, Mozilla, and Apple are all using the strategy with effectiveness. One needs deep pockets plus major connections to consumers and industry, though. Meanwhile, Python and Julia are examples (for me) of The Correct Thing with enough traits to make them successful despite lack of millions in funding, widespread industry support, etc. So, there's that approach too. Still an open topic where I have no definite answer. re seL4. Good luck on the ARM, kernel, and HOL learning projects. Will keep you busy for some time I imagine with make a few less hairs on your head after righting with hardware and kernel-level issues. ;) "Thanks a lot for this discussion and giving me hope WRT to intermediate ways to address the web browser problem!" You're welcome and thanks to you, too. It's been an interesting one. Do give me feedback on the Concrete Semantics and Isabelle stuff later so I can assess minimal level of talent that can use it.

by hga 11y ago

nickpsecurity 11y ago

It's funny you mentioned the PC losering problem because he countered his own claim later (see p3): https://www.dreamsongs.com/Files/worse-is-worse.pdf https://www.dreamsongs.com/Files/worse-is-worse.pdf The other stuff you mention are good for the time. Extra props for getting work done in direction of LISP machines. I could see that I'd have enjoyed using that system besides the odd quirks you mentioned. Plus, the name of the network is way cooler than the other guys'. ;) re Magnus/ML. I had CakeML in my collection but didn't know about Jitawa + Milawa. I remember skipping it seeing "verified lisp" in abstract while rushing through ACM/IEEE stuff and thinking "I already have VLISP so who cares." However, I appreciate your link because Milawa was a great find: an answer to the "Do you trust the prover?" question that people keep asking. Plus, Jitawa verifying a LISP and it were a nice combo. Knew Magnus was smart but that's extra smart. Anyway, looking at your update, I see CakeML now has a verified compiler and other cool stuff. I might stop recommending FLINT except for diversity. CakeML seems to be the one to build on with VeriML too limited imho: a portable compiler & runtime is always better than an interpreter for Getting Shit Done (TM). So, I appreciate that link. Your HOL work might be tricky. I'll be interested in hearing your experience later as it will inform how other software/systems people might fare. If it's difficult or even before you start, you might want to check out Chlipala's methodology here: http://adam.chlipala.net/cpdt/ http://adam.chlipala.net/cpdt/ It's more like the FLINT style than HOL. He's produced many solid works with that. His site (link on top) also has interesting tools for various use cases: Bedrock (verified assembly), Ur/Web (correct-by-construction web apps), contribute to Ynot (writing/verifying imperative code), and so on. What they built with it is obvious from descriptions. Their pace has been faster than full verification groups while knocking out lots of errors. There's also more investment of academic brains into Coq theorem prover so each work might benefit from others. Now, a link to help you with what you're actually doing. The seL4 work at some point referenced this book on using Isabelle/HOL for verification. Might be what you need to learn it all. I'd try it first. Stay on it if you're able to do real stuff w/ projects you referenced. Otherwise, backtrack to try Chlipala's methods. http://concrete-semantics.org/ http://concrete-semantics.org/ re browsers. Yes, they're critical for reasons you mentioned. There's a simple solution, though, which I used for years: physical separation w/ KVM switches and guards for information sharing. The browser stuff runs in a PC that handles it. Most of key work or trusted data on other system. The content is translated to formats that make verification easier or at least where you have trusted programs. The guard mediates flow of data to ensure files move back and forth without attacks on memory or transport. It's built as strong you can make it. KVM and drag-n-drop software make it easier to use. Tenix's Interactive Link is an implementation that's very similar. re Worse is Better & Java. I semi-agree. Java is a horrid platform that was successful for these reasons: (a) similarity to existing, mainstream languages, (b) tooling in form of IDE's + libraries, (c) perceived advantages, and mainly (d) massive money in marketing by huge, enterprise firm. So, the strategy worked. Google, Mozilla, and Apple are all using the strategy with effectiveness. One needs deep pockets plus major connections to consumers and industry, though. Meanwhile, Python and Julia are examples (for me) of The Correct Thing with enough traits to make them successful despite lack of millions in funding, widespread industry support, etc. So, there's that approach too. Still an open topic where I have no definite answer. re seL4. Good luck on the ARM, kernel, and HOL learning projects. Will keep you busy for some time I imagine with make a few less hairs on your head after righting with hardware and kernel-level issues. ;) "Thanks a lot for this discussion and giving me hope WRT to intermediate ways to address the web browser problem!" You're welcome and thanks to you, too. It's been an interesting one. Do give me feedback on the Concrete Semantics and Isabelle stuff later so I can assess minimal level of talent that can use it.