4 ms·

> because you're a novice, because you have better ways to spend your Saturday nights than disassembling core dumps My experience is that with a development me

> because you're a novice, because you have better ways to spend your Saturday nights than disassembling core dumps My experience is that with a development methodology that emphasizes early-binding, incremental testing, and aggressive factoring, I just don't have the same kinds of memory issues I do in C. Strings having an explicit length helps a lot, and I suspect stack manipulation having a linear-types-like feeling helps somewhat too, since you think a lot more about "should this be removing this from the stack" than "should I be using this variable again some time, you know, later." > because you're building a platform for safely running untrusted code written by players who are competing against one another, or because, given your own fallibility, you think it's the only way to be safe enough from ransomware gangs My aarch64 Forth runs under QEMU, and this is easy to set up, and wiring a PL011 to stdio works great. If you're just trying to avoid buffer overruns, though (which I suppose meets the latter case but not really the former), I'd consider using a 64-bit Forth with 32-bit pointers and 32-bit offsets, storing the size of the allocation in the first word before the pointer, so you can check the offset in a special TAGGED!/TAGGED@. I suspect you'd still want the normal !/@ for speed, and implement TAGGED!/TAGGED@ in terms of them, though? Perhaps the MTE extensions would work, but I haven't investigated them (I don't have a laptop whose CPU that supports them yet).

kragen 5y ago
> I just don't have the same kinds of memory issues I do in C. Interesting! I definitely haven't reached that level—in Forth I have the same kinds of memory problems I have in C, and also parameter-passing bugs and type errors. Is there a codebase you think of as exemplary that I could learn from? Or, maybe better, a screencast of somebody writing some software in the development style? (Interactive testing of new words doesn't leave development artifacts, after all.) "Much better than C" might still be pretty bad compared to JS, Rust, or OCaml; have you tried them? > My aarch64 Forth runs under QEMU, and this is easy to set up, and wiring a [UART] to stdio works great. This is definitely a viable approach that can work in many circumstances! However, each trust domain in QEMU uses 16 megabytes of RAM and roughly a million microseconds of CPU time to start up and shut down, and if you're doing cross-architecture emulation so you can't use kvm, the CPU overhead is typically on the order of 300%. By contrast, each trust domain in Lucet takes about 16 kilobytes of RAM and 50 microseconds of CPU time to start up and shut down https://www.fastly.com/blog/lucet-performance-and-lifecycle https://www.fastly.com/blog/lucet-performance-and-lifecycle, and a new trust domain in a language that implements object-capability security could conceivably take 16 bytes of RAM and 0.1 microseconds. In both cases you can usually come within a few percent of native-code performance—which probably isn't in the cards if every memory access is preceded by a bounds check, as in Valgrind (typically 1000% CPU overhead) or this pseudo-Forth approach. Communications round-trip time might be 1 μs per ping-pong in QEMU and 0.1 μs in the other cases. So, there are cases where a secure-compiler approach can give you 3–6 orders of magnitude better performance than just using QEMU. If you have a multiplayer game where each player uploads code, you might be able to support a few hundred players on a PC with the QEMU approach, or a few hundred thousand players with the Lucet approach. (Not, probably, all connected over TCP at once.) > consider using a 64-bit Forth with 32-bit pointers and 32-bit offsets An interesting idea here is to use a 64-bit system with 64-bit pointers and 32-bit offsets, mapping each allocation 4 gibibytes and change apart. Basically using the high 32 bits of the pointer as an MTE address tag or segment ID. Bloated and probably slow, though, and of course the bounds checking isn't very precise—enough to ensure that you can't index into another allocation, but not enough to catch every off-by-one array indexing bug. There used to be a fat-pointer bounds-checking version of GCC that replaced pointers with essentially Golang slices, and you could of course implement that kind of scheme on top of a standard Forth, much as you suggest with TAGGED@.
- remexre 5y ago
  > Is there a codebase you think of as exemplary that I could learn from? My "one codebase I keep rewriting" is [0]; I don't consider the artifact as useful as the process, though. Particularly, > in Forth I have the same kinds of memory problems I have in C, and also parameter-passing bugs and type errors. I find the memory problems are helped a lot by incremental testing in the REPL, as well as designing in such a way that it's obvious what a word does -- if a word has a surprising side-effect or requirement, that's a good sign some design rethinking is in order. Thinking Forth [1] has some examples of the kinds of redesigns that can be helpful, though as a warning it has strong "grumpy old man" vibes. I find these hilarious, but some don't :) (Some of its design suggestions are also somewhat "off" in my view; not a huge fan of DOER/MAKE, personally.) I definitely don't often experience parameter-passing bugs (assuming you mean "this takes 3 args, thought it took 2") nor type errors, and I'm actually a bit surprised to hear you do. I suppose I rather religiously stack comment, and write just about every word to have a "static" stack effect. I've also got a shell alias: ffd() { rg -FiIN ": $1 (" "${2:-$HOME/Projects/stahl/kernel/src}" }; so I can just quickly do e.g. $ ffd nip : NIP ( a b -- b ) SWAP DROP ; $ ffd allocate-pages : ALLOCATE-PAGES ( num-pages -- 0 0 | addr -1 ) I ought to set keywordprg in Vim to that too, then I could get it in-editor. Of course, this doesn't work for builtins and control constructs -- perhaps someday I'll have the compiler put the pointer in SOURCE in the word header, and write a language server that looks through them. > [...] JS, Rust, or OCaml; have you tried them? Yeah, more the latter two than JS. Maintaining memory safety is easier in a memory-safe language, but I'm not certain overall correctness and design simplicity is. Certainly, when I'm implementing things in OCaml, I feel like I have to make design compromises much more than in Forth (where Forth gives me more room to redesign instead of getting forced into an unideal compromise). Rust's macros give me a bunch more leeway, but it's still occasionally awkward to express some things where something really is just easier to express at runtime, but it's impossible or UB/unsound to do so. Common Lisp is perhaps a better competitor in this regard, since like Forth it supports both powerful compile-time and run-time metaprogramming. Maybe MetaOCaml too, though I've yet to try it. > However, each trust domain in QEMU [...] Yeah, of course QEMU isn't a silver bullet in this regard; if your application needs to be able to spawn large numbers of sandboxes quickly, especially. If you wanted to push virtualization as far as it could go, I'd consider the rust-vmm/Firecracker work instead -- they have stock Linux booting in 250ms/core, and a (perhaps custom) ringbuffer shared between the two processes would of course be vastly lower overhead than proper emulation of hardware. > [...] Lucet [...] I actually considered dropping WASM in initially, but I removed it after remembering my experience with trying to do JITtish things in it -- it's not currently practical (as of like a year ago) to do a DTC Forth, or a Forth that inlines, in WASM, since words are just too small. WASM being an "extreme" Harvard architecture is also fairly annoying. I suppose an ITC Forth ought to work, but without an inliner, performance seems like it'd be fairly bad. I believe there's an API in spec-development currently to add better primitives for JIT that's sized closer to a basic block, so maybe that would change the situation. > [...] object-capability security [...] If you're going that... high-level? abstract? why not use Factor? I think, as you describe above, a Smalltalk-inspired approach might be a better foundation than most Forths' "assembly-inspired" ones. Though, as I understand it (too young to have lived through it!), Smalltalk had awful performance until Self came along and invented modern JIT, by which point you've completely lost the virtue of simplicity of implementation (at which point I'd be biased to say, you should use a Lisp or Haskell variant instead!) > [...] 64-bit pointers [...] Yeah, I considered a variation of that (most memory bugs are off-by-n for a small n, so guard pages are almost as good), but having a minimum allocation size of 4k seemed too wasteful. > [...] replaced pointers [...] Oh, I think TCC [2] still implements that! My understanding was that doing that relied on the sorts of C UB rules that some people hate (and that I quite like that Forth lacks!) though. I suppose if sizeof(uintptr_t) == 2*sizeof(ptrdiff_t), that wouldn't need to use the rules, but I think that'd suck pretty bad in Forth. --- I think there are (at least!) two axes being compared here: 1. How easy is it to write correct Forth (I include security in correctness -- arbitrary code execution is typically pretty incorrect!) 2. How easy is it to execute attacker-provided Forth safely I'd say Forth is strongly competitive on the first axis, and isn't at all on the second. I'd certainly believe that Factor or a Smalltalk-like Forth could be competitive on the latter, but if you include bugs in the compiler and runtime as correctness violations, I suspect it'd suffer a lot on the first axis. I've thought a bit about getting stronger assurances of correctness for my Forth programs without complexifying the implementation of the system (which would make incorrectness much more likely). Currently I'm thinking about doing proofs in separation logic, with symbolic execution acting to hopefully provide a high degree of proof automation. An important characteristic is doing these proofs on the program starting at some physical machine state at a fixed time (e.g. just before some main loop is entered), rather than on the abstract machine that the runtime and compiler hopefully implement correctly. I think the system is simple enough that no mismatch between the two would occur, but I suppose I'll see whenever I've finished learning enough to start implementing this. --- [0]: https://git.sr.ht/~remexre/stahl/tree/main/item/kernel/src https://git.sr.ht/~remexre/stahl/tree/main/item/kernel/src [1]: https://managedway.dl.sourceforge.net/project/thinking-forth/reprint/rel-1.0/thinking-forth-color.pdf?viasf=1 https://managedway.dl.sourceforge.net/project/thinking-forth... [2]: https://bellard.org/tcc/ https://bellard.org/tcc/

kragen 5y ago

> I just don't have the same kinds of memory issues I do in C. Interesting! I definitely haven't reached that level—in Forth I have the same kinds of memory problems I have in C, and also parameter-passing bugs and type errors. Is there a codebase you think of as exemplary that I could learn from? Or, maybe better, a screencast of somebody writing some software in the development style? (Interactive testing of new words doesn't leave development artifacts, after all.) "Much better than C" might still be pretty bad compared to JS, Rust, or OCaml; have you tried them? > My aarch64 Forth runs under QEMU, and this is easy to set up, and wiring a [UART] to stdio works great. This is definitely a viable approach that can work in many circumstances! However, each trust domain in QEMU uses 16 megabytes of RAM and roughly a million microseconds of CPU time to start up and shut down, and if you're doing cross-architecture emulation so you can't use kvm, the CPU overhead is typically on the order of 300%. By contrast, each trust domain in Lucet takes about 16 kilobytes of RAM and 50 microseconds of CPU time to start up and shut down https://www.fastly.com/blog/lucet-performance-and-lifecycle https://www.fastly.com/blog/lucet-performance-and-lifecycle, and a new trust domain in a language that implements object-capability security could conceivably take 16 bytes of RAM and 0.1 microseconds. In both cases you can usually come within a few percent of native-code performance—which probably isn't in the cards if every memory access is preceded by a bounds check, as in Valgrind (typically 1000% CPU overhead) or this pseudo-Forth approach. Communications round-trip time might be 1 μs per ping-pong in QEMU and 0.1 μs in the other cases. So, there are cases where a secure-compiler approach can give you 3–6 orders of magnitude better performance than just using QEMU. If you have a multiplayer game where each player uploads code, you might be able to support a few hundred players on a PC with the QEMU approach, or a few hundred thousand players with the Lucet approach. (Not, probably, all connected over TCP at once.) > consider using a 64-bit Forth with 32-bit pointers and 32-bit offsets An interesting idea here is to use a 64-bit system with 64-bit pointers and 32-bit offsets, mapping each allocation 4 gibibytes and change apart. Basically using the high 32 bits of the pointer as an MTE address tag or segment ID. Bloated and probably slow, though, and of course the bounds checking isn't very precise—enough to ensure that you can't index into another allocation, but not enough to catch every off-by-one array indexing bug. There used to be a fat-pointer bounds-checking version of GCC that replaced pointers with essentially Golang slices, and you could of course implement that kind of scheme on top of a standard Forth, much as you suggest with TAGGED@.

remexre 5y ago
> Is there a codebase you think of as exemplary that I could learn from? My "one codebase I keep rewriting" is [0]; I don't consider the artifact as useful as the process, though. Particularly, > in Forth I have the same kinds of memory problems I have in C, and also parameter-passing bugs and type errors. I find the memory problems are helped a lot by incremental testing in the REPL, as well as designing in such a way that it's obvious what a word does -- if a word has a surprising side-effect or requirement, that's a good sign some design rethinking is in order. Thinking Forth [1] has some examples of the kinds of redesigns that can be helpful, though as a warning it has strong "grumpy old man" vibes. I find these hilarious, but some don't :) (Some of its design suggestions are also somewhat "off" in my view; not a huge fan of DOER/MAKE, personally.) I definitely don't often experience parameter-passing bugs (assuming you mean "this takes 3 args, thought it took 2") nor type errors, and I'm actually a bit surprised to hear you do. I suppose I rather religiously stack comment, and write just about every word to have a "static" stack effect. I've also got a shell alias: ffd() { rg -FiIN ": $1 (" "${2:-$HOME/Projects/stahl/kernel/src}" }; so I can just quickly do e.g. $ ffd nip : NIP ( a b -- b ) SWAP DROP ; $ ffd allocate-pages : ALLOCATE-PAGES ( num-pages -- 0 0 | addr -1 ) I ought to set keywordprg in Vim to that too, then I could get it in-editor. Of course, this doesn't work for builtins and control constructs -- perhaps someday I'll have the compiler put the pointer in SOURCE in the word header, and write a language server that looks through them. > [...] JS, Rust, or OCaml; have you tried them? Yeah, more the latter two than JS. Maintaining memory safety is easier in a memory-safe language, but I'm not certain overall correctness and design simplicity is. Certainly, when I'm implementing things in OCaml, I feel like I have to make design compromises much more than in Forth (where Forth gives me more room to redesign instead of getting forced into an unideal compromise). Rust's macros give me a bunch more leeway, but it's still occasionally awkward to express some things where something really is just easier to express at runtime, but it's impossible or UB/unsound to do so. Common Lisp is perhaps a better competitor in this regard, since like Forth it supports both powerful compile-time and run-time metaprogramming. Maybe MetaOCaml too, though I've yet to try it. > However, each trust domain in QEMU [...] Yeah, of course QEMU isn't a silver bullet in this regard; if your application needs to be able to spawn large numbers of sandboxes quickly, especially. If you wanted to push virtualization as far as it could go, I'd consider the rust-vmm/Firecracker work instead -- they have stock Linux booting in 250ms/core, and a (perhaps custom) ringbuffer shared between the two processes would of course be vastly lower overhead than proper emulation of hardware. > [...] Lucet [...] I actually considered dropping WASM in initially, but I removed it after remembering my experience with trying to do JITtish things in it -- it's not currently practical (as of like a year ago) to do a DTC Forth, or a Forth that inlines, in WASM, since words are just too small. WASM being an "extreme" Harvard architecture is also fairly annoying. I suppose an ITC Forth ought to work, but without an inliner, performance seems like it'd be fairly bad. I believe there's an API in spec-development currently to add better primitives for JIT that's sized closer to a basic block, so maybe that would change the situation. > [...] object-capability security [...] If you're going that... high-level? abstract? why not use Factor? I think, as you describe above, a Smalltalk-inspired approach might be a better foundation than most Forths' "assembly-inspired" ones. Though, as I understand it (too young to have lived through it!), Smalltalk had awful performance until Self came along and invented modern JIT, by which point you've completely lost the virtue of simplicity of implementation (at which point I'd be biased to say, you should use a Lisp or Haskell variant instead!) > [...] 64-bit pointers [...] Yeah, I considered a variation of that (most memory bugs are off-by-n for a small n, so guard pages are almost as good), but having a minimum allocation size of 4k seemed too wasteful. > [...] replaced pointers [...] Oh, I think TCC [2] still implements that! My understanding was that doing that relied on the sorts of C UB rules that some people hate (and that I quite like that Forth lacks!) though. I suppose if sizeof(uintptr_t) == 2*sizeof(ptrdiff_t), that wouldn't need to use the rules, but I think that'd suck pretty bad in Forth. --- I think there are (at least!) two axes being compared here: 1. How easy is it to write correct Forth (I include security in correctness -- arbitrary code execution is typically pretty incorrect!) 2. How easy is it to execute attacker-provided Forth safely I'd say Forth is strongly competitive on the first axis, and isn't at all on the second. I'd certainly believe that Factor or a Smalltalk-like Forth could be competitive on the latter, but if you include bugs in the compiler and runtime as correctness violations, I suspect it'd suffer a lot on the first axis. I've thought a bit about getting stronger assurances of correctness for my Forth programs without complexifying the implementation of the system (which would make incorrectness much more likely). Currently I'm thinking about doing proofs in separation logic, with symbolic execution acting to hopefully provide a high degree of proof automation. An important characteristic is doing these proofs on the program starting at some physical machine state at a fixed time (e.g. just before some main loop is entered), rather than on the abstract machine that the runtime and compiler hopefully implement correctly. I think the system is simple enough that no mismatch between the two would occur, but I suppose I'll see whenever I've finished learning enough to start implementing this. --- [0]: https://git.sr.ht/~remexre/stahl/tree/main/item/kernel/src https://git.sr.ht/~remexre/stahl/tree/main/item/kernel/src [1]: https://managedway.dl.sourceforge.net/project/thinking-forth/reprint/rel-1.0/thinking-forth-color.pdf?viasf=1 https://managedway.dl.sourceforge.net/project/thinking-forth... [2]: https://bellard.org/tcc/ https://bellard.org/tcc/