The Unclear Impact

Kristóf Marussy ferdi | @kristof@pleroma.marussy.com

I'm a PhD student working on the extra-functional requirements and formal verification of cyber-physical system architectures.
I also like free (as in liberty) software, privacy enhancing technologies, and cryptography.

@fedops @robby sshfs is yet another different thing (and another awesome use-case for ssh!)

I’m more interested about having some authenticated tunnel for a bunch of streams (tcp connection, named piped, etc.). which is served mostly nicely by either ssh port forwarding or just piping some command’s stdin/stdout over ssh, but could probably still be improved (e.g., by making it tolerant agains network failure à la mosh)

@robby Yeah, SSH’s pretty cool, but it sometimes feels like it would be better to separate the authentication/tunneling/communication channels (it’s awkward that you can forward ports, but not file descriptors/pipes, so any piping for btrfs send and the like has to be done over the standard io or maybe netcat) functionality from the terminal functionality. I guess mosh does the terminal thing pretty well (piggybacking on ssh for authentication and a pipe to receive connection info), but there’s no tool that just wants to be an authenticated pipe thing. Overlay networks like nebula are similar, but they generally need root access to set up a network, and also only work with ports. (Although that’s probably just me moaning about my ridiculously specific use-case for a user-mode overlay network.)

academia, reviewing

just wrote a 12k character review about the reproducibility of an artifact. granted, 7k of that is the diff -u between the output claimed by the authors and the actual output on my system, but it might still be a bit excessive (on the other hand, I hope that correcting the discrepancies will improve the associated paper)

re: category theory, programming languages, long

@hazel Mathematicians like to use a lot of abstract algebra to get intuition for category theory (and that’s the historic route), but I always found such presentations incomprehensible (because I’m not a mathematician). On the other extreme, the kind of stuff in Category Theory for Programmers is a nice introduction, but is a bit misleading if just skimmed (wasn’t really obvious to me why don’t we simply do everything with sets).

What really made it click for me was programming language semantics. I was once at a summer school on probabilistic programming: Dexter Kozen on the foundations of semantics with (\omega)-CPOs, Prakash Panangaden on the Giry monad (probability theory, but with more categories), and Hongseok Yang on Yoneda embedding for higher-order probabilistic programs (I think even he admits that it’s overkill, but there’s a way to simplify it). Of course, we were a room a confused first-year PhD students with nonexistent category theory background, so most of it didn’t stick, but re-reading CT4P afterwards made a bit more sense.

It’s cool to be able to replace sets with basically any structure you want and do semantics that way. As a bonus, (\omega)-CPOs are supposed to be the way to make Hask actually into a category.

Although this just replaces the need for an abstract algebra background with the need for a probability theory background (or a background in the semantics of something equally weird you want to program). But it might be a bit more concrete payoff.

As for type theory, this could be useful up to the point you need to work with semantics in type theory papers, but that’s not necessarily modern.

There should be an overlay networking thing like nebula, but without the need for a tun interface, just with forwarded ports à la ssh.

Although I’m fully aware that the tun interface is what makes nebula fast.

@TinfoilSubmarine Unfortunately, the complex chaining of forwarding doesn’t seem to work too well, and leads to the et process crashing if the reverse tunnel being tunneled to my laptop breaks. Also, my phone company doesn’t seem to provide IPv6 over 4G (or at least Termux can’t use it), and it seems to default to using that instead of IPv4 with no fallback on error.

@TinfoilSubmarine My main reason for trying it out instead of mosh was that is supports port forwarding. But I haven’t set that up yet, so we’ll see.

The idea would be to reverse-tunnel the ssh and EternalTerminal ports from my phone to my VPS, then tunnel the same ports from my VPS to my laptop, and be able to connect from my laptop to my phone even if my phone is on a firewalled wifi (at uni). Which is a bit of overengineering, to say the least, but initially sounded fun. blobfoxlaughsweat

EternalTerminal is pretty cool, it’s a pity it has opt-out telemetry

(to opt out, define ET_NO_TELEMETRY=1 and pass --telemetry=false to the client and set [Debug] Telemetry = 0 in /etc/et.cfg on the server)

@jookia to be fair, compiling a rust application with less than 200 MiB of free RAM wasn’t the best of ideas from me, even without an oom killer

it’s ‘fun’ when the oom-killer kills sshd, so I can’t fix whatever is eating the memory remotely

anyways, updated my VPS from 2GiB of RAM to 4GiB, hopefully no more oom-killing blobfoxrage

academia, cloud, shitpost

does the ACM (Association for Computing Machinery) use ACM (AWS Certificate Manager) to manage their certificates in AWS? blobfoxthinkgoogly

re: arch linux

@kristof nope. it also doesn't support things like eye tracking and other stuff.

shim does not support being managed by a rich OS either, so you can't add keys that way

i opened an issue about this but it's been crickets

re: arch linux

@kristof yeah but like, even now it's not possible to add manual keys for disabled people

re: arch linux

@jookia yeah, in general, the UEFI menus seem to have abysmal accessibility. is it possible at all to, say, use a screen reader when changing boot settings?

re: arch linux

@jookia indeed, and that’s a grand shame blobfoxnotamused

re: arch linux

@jookia I mean that having to manage passwords is considered perfectly normal (after all, people usually log in to their accounts with a password), yet managing keys is considered strange and difficult.

If we, e.g., moved to hardware tokens instead of passwords everywhere, we could make managing keys for your hardware as easy as managing logins for websites. From the point of view of a smart card, the two aren’t that dissimilar, anyways. From the point of view of the average user, they’d simply be compelled to safekeep their token instead of a piece of paper with their password on it.

re: arch linux

@jookia We should normalize key management for end users

re: arch linux

@jookia I consider removing Microsoft keys (and thus the ability to remotely attest the integrity of a Windows system) crucial in the fight against DRM. (Only ironically, though, because removing the key from a single machine does fuck all against DRM. But would be cool if everyone used their own keys.)

re: arch linux

@jookia It works perfectly well with your own keys (the only type of key that should matter): https://wiki.archlinux.org/title/Unified_Extensible_Firmware_Interface/Secure_Boot#Using_your_own_keys

new blog post!

# Software From Another World

> We undermine not only unions, but every aspect of the worker's life: AirBnB spikes rents, Uber disenfranchises drivers, a thousand streaming services reinvent cable, Amazon fucks everybody, and so on. Despite any niche expertise, these are companies made possible by software, by the lending of software labor to capitalist ends. We can choose to deny them, if we stand together.

https://garbados.github.io/my-blog/software_from_another_world.html

»