9 ms·

If you may spare a minute, I'd like to know your opinion on mission-critical software in dangerous-prone contexts (such as avionics, life support, even just eco

by K0SM0S 7y ago

If you may spare a minute, I'd like to know your opinion on mission-critical software in dangerous-prone contexts (such as avionics, life support, even just economically for permanently-written "ROM" software, etc). Formal methods seem required in such projects, but your final paragraph seems to imply the formalism isn't key to end quality? (my agenda, for transparency: I want to send SOC's in space on tiny RISC-V satellites, and the lowest layers of those should be 100% error-free because there's no going physically there to reboot a working shell, remote is all we have.) Regarding 'love' for blockchain, I think it's the basic proposition of "100% accurate data that cannot be controlled by anyone" that seduces. The 'cost' of that in performance becomes a nagging second concern. It gives people a feeling of safety if no other party, not their bank nor family nor employer nor anyone can alter their data, their transactions (whatever the kind, financial is but one use). Whether blockchain is the only way to achieve that is another matter, but (afaik?) so far it's the only working implementation of the concept of perfectly secured data. I think that's what drove people nuts. I also think Bitcoin or currency in general is but one use case and a very impractical one in the current financial environment, i.e. Earth circa 2019. I'd wager there are much better avenues to explore, eminently non-financial in nature, such as peer-to-peer 'free' communication, or formal (law, contracts) codification (anything official and 'forever' until 'revoked'). No coin, no market, no whatever but the benefits of a slow but 100% truthful database, for small data (text fits quite well).

kragen 7y ago
> (my agenda, for transparency: I want to send SOC's in space on tiny RISC-V satellites, and the lowest layers of those should be 100% error-free because there's no going physically there to reboot a working shell, remote is all we have.) Speaking from a bit of experience at Satellogic as well as folklore, trying to make the lowest levels 100% error-free isn't a good strategy. A better strategy is to make the lowest levels capable of recovering from the errors that will occur most frequently. Radiation is going to flip bits; processors are going to fail and sometimes hang; batteries are going to go low; temperatures are going to exceed specifications. If your system is built on the assumption that the lowest layers are going to be 100% error-free, you won't give sufficient attention to handling those errors when your assumption inevitably turns out to be wrong. One suggestion: include a remotely-triggerable reset sequence in a hardware state machine. A 4-bit state machine driven by 4-bit symbols will work reliably if your channel error rate is small compared to one error per 16 symbols, and it has a false positive trigger rate of 5.4 × 10⁻²⁰. (This is of course vulnerable to malicious DoS attacks if a malicious party learns the 64-bit reset code, but in practice those have historically been an enormously smaller concern than satellites failing randomly in ways that a reset switch can correct.) It's worth thinking through the fault tree of that reset mechanism. It needs to use omnidirectional antennas, for example, because otherwise it's dependent on attitude control. It needs to be on all the time, not just when you're passing over ground stations, because otherwise it depends on the clock and whatever kind of navigational system you have. It needs to be unencrypted, because otherwise it depends on your encryption protocol, which typically also involves clocks. It unavoidably depends on some kind of power source, but you can connect it directly to the solar panels and/or batteries, rather than through a switch. You probably want to use logic that can tolerate a fair bit of uncontrolled variation of the power supply voltage, not, say, TTL. But then you need like 4 flip-flops and a couple dozen gates. It can fail, but it's simple enough that you can make it highly reliable, unlike a RISC-V. So, don't think in terms of making the bottom level 100% reliable. You won't get there. Think in terms of how to prevent inevitable unreliability from snowballing, how to make the satellite resilient against inevitable damage and malfunctions, as well as reducing that bottom-level unreliability to an absolute minimum. As for blockchains, I think they're a very pragmatic solution to serious problems that are otherwise unsolvable: how can I send money to a friend in Venezuela? How can refugees carry their money safely without it being confiscated by pirates, corrupt police, or immigration authorities? How can people pay for illegal drugs without meeting in person with the vendors? How can we fund Wikileaks so they have the resources to transport Ed Snowden to safety? How can we fund Sci-Hub so that knowledge is available to everyone and not lost? Even international remittances to family members work enormously better with Bitcoin than with Western Union or SWIFT, particularly between countries with some degree of unfriendly relations. It's a similar approach to that with satellites: we know there are bad actors in the financial system, and we want to engage in transactions with them, without giving them the opportunity to sell our credit card numbers to the Russian Mafia or take all our money. We want to prevent the small amounts of inevitable unreliability from snowballing and destroying the entire civilization. Also, we want to minimize the number of attempted ripoffs, so that our defenses against them can be less costly. It turns out that thieves, unlike cosmic rays, respond to incentives, so by making thefts more difficult to pull off, we can also decrease the number of attempted thefts. Obviously I don't trust Facebook to design the world financial system, though. They elected Trump.
- K0SM0S 7y ago
  Thanks so much for all the food for thought and recommendations. I had a hunch for "capable of recovering", and now I have a clearer roadmap (some critical steps). I see your way of thinking. This in particular: > Think in terms of how to prevent inevitable unreliability from snowballing, how to make the satellite resilient against inevitable damage and malfunctions, as well as reducing that bottom-level unreliability to an absolute minimum. High-availability of components seems like a given to me (e.g. have 2, 3, 4 batteries as distant from each other as possible, to mitigate loss if one gets shot by some collision or outright fails; rinse and repeat for every critical component, starting at circuit design). In another comment, user "pjc50" suggests to me “"lockstep" chips, such as TI Hercules”, and yet my intuition would be to put two redundant ones on each satellite, just for good measure. But the ultimate economics of the project can be made to work, imho, because I envision a swarm of such tiny satellites actually, wherein you can afford to lose a few nodes now and then, if that makes all of them orders of magnitude cheaper — and thus you can send orders of magnitude more, overall. Brute-force the reliability issue by making them expendable to a reasonable degree. No human life means they can die for all we care, if it makes sense cost-wise. Hence why in that perspective, a discussion on the cost versus benefit of formal methods is of great interest. Needless to say, any advanced draft of the project would inevitably have to be vetted by, actually co-developed with field experts like you. To each contributor their domain. I hope it will be a given too, since I'm thinking of a 100% open-source project (both software and hardware ideally). The more eyeballs... ____ I see your points about blockchain, and they make a lot of sense; the problem I see with current 'cryptos' in general (including the big one) is that they simply aren't welcomed by most decisive institutions, including those who combat on principle the problems you mention. Like, you see the EFF et. al defending e.g. E2E encryption, but none of that drive to promote bitcoin. Thus that 'respectable' cryptocurrencies exist to solve these problems, sure, please, yesterday! — but that they reform the financial system by their very existence? There doesn't seem to be much appeal in the mainstream. I think it's a matter of time, how much each generation weighs demographically in the global opinion / decision power. For now, it's boomers, and they're not in that place.
  - kragen 7y ago
    I'm not a field expert; I didn't design Satellogic's satellites. Satellogic's CubeBug design did use a TI Hercules TMS570 Cortex-R, and I think it's safe to say our experiences with chips like that were good — for the relatively restricted tasks they can perform. The automotive industry has a lot of lockstep chips available for it, because it's a mass market that demands reliability under harsh conditions. I'd like to point out that what you're describing is pretty similar to Satellogic's original business plan.
hypertexthero 7y ago
Regarding mission-critical software in dangerous-prone contexts, there is good information from experts from the Apollo program on http://www.htius.com/ http://www.htius.com/
- K0SM0S 7y ago
  Ha! interesting, thank you for the link. Edit: skimming through the paper, really really solid material. Much appreciated.
blotter_paper 7y ago
> my agenda, for transparency: I want to send SOC's in space on tiny RISC-V satellites I've seen your posts in multiple threads K0SM0S, and I generally enjoy reading your thoughts and opinions. When I meet people I find interesting, I like to ask what they plan on doing with their lives. I understand completely if you don't want to share further details, but I for one would be interested in an off-topic detour into your intentions with these microsatellites. One application I always toy with in my head is a time+location verification service, but I don't think satellites are strictly necessary for that one unless you're trying to work around region-specific laws that would regulate towers.
- K0SM0S 7y ago
  Hi, I'm not sure if you'll get this late reply. First of all, thank you so much for your kind words, they mean the world to me, and for your interest — which is now reciprocal, I want to hear about you as well!.. I must admit I've spent way too much time trying to answer your questions in a 'concise' manner —HN's norm— but, as usual with this topic, it proved unusually hard fo me. It's rather complex, several independent yet synergistic 'moving parts' — too much repetition and cognitive bloat for a mere comment. Thus I'm drafting something to share and discuss the concepts, if time permits it'll be up on some website (maybe reddit, maybe a forum, maybe some blog, idk...) by month's end. I'll keep you updated, if you so wish. You can reach me by email `cosmos// a t //vcx.cx` ;-) The gist of it, FYI: - the satellite thing is a personal research project (in very tangible ways, the experiment is to actually do it and launch). But the endgame (think 2030-2040) is a massive swarm of ~8 billion devices or more, if you catch my drift. - However, it's an extension to a ground network which essentially aims at being an alternative infrastructure to internet. Formally it's something along the lines of a distributed, decentralized ("peer-to-peer") mesh network, fully encrypted yadi yada. - This network is but an "optional" medium for my original idea (in ~2010) which was, in dumb terms, a communication network (which people would call 'social network' I guess, but it's not against such existing services, it's more of a global standard / spec whose primary goals are security/freedom/privacy, interoperability (like email), and to be 'unstoppable' (in the event of war, catastrophe, etc). Going back to first principles, this 'network' is not even an application but a formal protocol I suppose. It's the kind of thing that would ideally exist as an RFC 'standard' by the IETF. This is more generally motivated by some of my philosophical values, notably freedom, empowering individuals (in the name of progress, civilization, but also happiness, self-growth).
pron 7y ago
> but your final paragraph seems to imply the formalism isn't key to end quality? That's not what I said. I said that merely creating a verified formal specification of a language is not in itself a good path to increasing correctness, and I wouldn't focus on that as a significant cause for concern given all others. But even when you use formal methods in the development of your software -- and I'm certainly a proponent -- there are many formal methods with widely different guarantees and costs, and some of them don't require a formal specification of the programming language. Moreover, no system can be 100% error free, regardless of verification method used. Systems rely on hardware whose actual behavior can never be "proven" correct, and, at best, only probabilistically matches the spec. I personally believe that some formal methods can greatly improve correctness, and do so affordably, but the question of which formal methods are worthwhile when and by how much each of them improves correctness is very much an open question. > it's the only working implementation of the concept of perfectly secured data. I strongly disagree. There is no such thing as "perfectly secure." Security is defined with respect to certain threats (e.g. a hazmat suit can protect you from poisonous gas but gives you no defense from bullets, whereas a bullet-proof vest is the opposite), and blockchain is rarely the most secure with respect to the most relevant threats in a monetary system.
- AlphaWeaver 7y ago
  > Security is defined with respect to certain threats, and blockchain is rarely the most secure with respect to the threats in a monetary system. Wow, this is a great way to frame this! What do you see as the largest threats to the effective operation of a monetary system?
  - pron 7y ago
    I think this question is best answered by economists, and I'm certainly not one. But blockchain does seem to interfere with some of the best regulatory defenses against economic disasters.
    - rossdavidh 7y ago
      Blockchain gives the impression that the primary threat it is designed to defend against, is a government deciding (like Germany between world wars) to inflate their currency for whatever reason. So, not surprisingly, in order to defend a currency against being decreased in value by a central authority, it is vulnerable to all of the threats that a central monetary authority might help you with. Which of these threats you think is the more salient is, of course, a matter on which people may disagree. I personally find the risk of a central monetary authority devaluing my money, to be not one of my top concerns, but I could understand why others might think differently (especially if they were in a different country, that used a different currency).
ukj 7y ago
Beware of bugs in the above code; I have only proved it correct, not tried it. --Donald Knuth On the one hand we have the management mantra: if you can't measure it you can't improve it. On the other hand we have Goodhart's law. And so 'correctness', 'safety', 'quality' (or absence thereof) are fluid concepts that can never be formalised precisely. Language/logic sucks, but it's all we've got.
- pron 7y ago
  > Language/logic sucks, but it's all we've got. Perhaps, but PLT is not the main discipline studying software correctness -- those would be formal methods and software engineering -- although it has some overlap with those disciplines. PLT is not the general name for all study of programs; it is the name for a particular perspective, and a particular component of that study.

by K0SM0S 7y ago

kragen 7y ago

> (my agenda, for transparency: I want to send SOC's in space on tiny RISC-V satellites, and the lowest layers of those should be 100% error-free because there's no going physically there to reboot a working shell, remote is all we have.) Speaking from a bit of experience at Satellogic as well as folklore, trying to make the lowest levels 100% error-free isn't a good strategy. A better strategy is to make the lowest levels capable of recovering from the errors that will occur most frequently. Radiation is going to flip bits; processors are going to fail and sometimes hang; batteries are going to go low; temperatures are going to exceed specifications. If your system is built on the assumption that the lowest layers are going to be 100% error-free, you won't give sufficient attention to handling those errors when your assumption inevitably turns out to be wrong. One suggestion: include a remotely-triggerable reset sequence in a hardware state machine. A 4-bit state machine driven by 4-bit symbols will work reliably if your channel error rate is small compared to one error per 16 symbols, and it has a false positive trigger rate of 5.4 × 10⁻²⁰. (This is of course vulnerable to malicious DoS attacks if a malicious party learns the 64-bit reset code, but in practice those have historically been an enormously smaller concern than satellites failing randomly in ways that a reset switch can correct.) It's worth thinking through the fault tree of that reset mechanism. It needs to use omnidirectional antennas, for example, because otherwise it's dependent on attitude control. It needs to be on all the time, not just when you're passing over ground stations, because otherwise it depends on the clock and whatever kind of navigational system you have. It needs to be unencrypted, because otherwise it depends on your encryption protocol, which typically also involves clocks. It unavoidably depends on some kind of power source, but you can connect it directly to the solar panels and/or batteries, rather than through a switch. You probably want to use logic that can tolerate a fair bit of uncontrolled variation of the power supply voltage, not, say, TTL. But then you need like 4 flip-flops and a couple dozen gates. It can fail, but it's simple enough that you can make it highly reliable, unlike a RISC-V. So, don't think in terms of making the bottom level 100% reliable. You won't get there. Think in terms of how to prevent inevitable unreliability from snowballing, how to make the satellite resilient against inevitable damage and malfunctions, as well as reducing that bottom-level unreliability to an absolute minimum. As for blockchains, I think they're a very pragmatic solution to serious problems that are otherwise unsolvable: how can I send money to a friend in Venezuela? How can refugees carry their money safely without it being confiscated by pirates, corrupt police, or immigration authorities? How can people pay for illegal drugs without meeting in person with the vendors? How can we fund Wikileaks so they have the resources to transport Ed Snowden to safety? How can we fund Sci-Hub so that knowledge is available to everyone and not lost? Even international remittances to family members work enormously better with Bitcoin than with Western Union or SWIFT, particularly between countries with some degree of unfriendly relations. It's a similar approach to that with satellites: we know there are bad actors in the financial system, and we want to engage in transactions with them, without giving them the opportunity to sell our credit card numbers to the Russian Mafia or take all our money. We want to prevent the small amounts of inevitable unreliability from snowballing and destroying the entire civilization. Also, we want to minimize the number of attempted ripoffs, so that our defenses against them can be less costly. It turns out that thieves, unlike cosmic rays, respond to incentives, so by making thefts more difficult to pull off, we can also decrease the number of attempted thefts. Obviously I don't trust Facebook to design the world financial system, though. They elected Trump.

K0SM0S 7y ago
Thanks so much for all the food for thought and recommendations. I had a hunch for "capable of recovering", and now I have a clearer roadmap (some critical steps). I see your way of thinking. This in particular: > Think in terms of how to prevent inevitable unreliability from snowballing, how to make the satellite resilient against inevitable damage and malfunctions, as well as reducing that bottom-level unreliability to an absolute minimum. High-availability of components seems like a given to me (e.g. have 2, 3, 4 batteries as distant from each other as possible, to mitigate loss if one gets shot by some collision or outright fails; rinse and repeat for every critical component, starting at circuit design). In another comment, user "pjc50" suggests to me “"lockstep" chips, such as TI Hercules”, and yet my intuition would be to put two redundant ones on each satellite, just for good measure. But the ultimate economics of the project can be made to work, imho, because I envision a swarm of such tiny satellites actually, wherein you can afford to lose a few nodes now and then, if that makes all of them orders of magnitude cheaper — and thus you can send orders of magnitude more, overall. Brute-force the reliability issue by making them expendable to a reasonable degree. No human life means they can die for all we care, if it makes sense cost-wise. Hence why in that perspective, a discussion on the cost versus benefit of formal methods is of great interest. Needless to say, any advanced draft of the project would inevitably have to be vetted by, actually co-developed with field experts like you. To each contributor their domain. I hope it will be a given too, since I'm thinking of a 100% open-source project (both software and hardware ideally). The more eyeballs... ____ I see your points about blockchain, and they make a lot of sense; the problem I see with current 'cryptos' in general (including the big one) is that they simply aren't welcomed by most decisive institutions, including those who combat on principle the problems you mention. Like, you see the EFF et. al defending e.g. E2E encryption, but none of that drive to promote bitcoin. Thus that 'respectable' cryptocurrencies exist to solve these problems, sure, please, yesterday! — but that they reform the financial system by their very existence? There doesn't seem to be much appeal in the mainstream. I think it's a matter of time, how much each generation weighs demographically in the global opinion / decision power. For now, it's boomers, and they're not in that place.
- kragen 7y ago
  I'm not a field expert; I didn't design Satellogic's satellites. Satellogic's CubeBug design did use a TI Hercules TMS570 Cortex-R, and I think it's safe to say our experiences with chips like that were good — for the relatively restricted tasks they can perform. The automotive industry has a lot of lockstep chips available for it, because it's a mass market that demands reliability under harsh conditions. I'd like to point out that what you're describing is pretty similar to Satellogic's original business plan.

hypertexthero 7y ago

Regarding mission-critical software in dangerous-prone contexts, there is good information from experts from the Apollo program on http://www.htius.com/ http://www.htius.com/

K0SM0S 7y ago
Ha! interesting, thank you for the link. Edit: skimming through the paper, really really solid material. Much appreciated.

blotter_paper 7y ago

> my agenda, for transparency: I want to send SOC's in space on tiny RISC-V satellites I've seen your posts in multiple threads K0SM0S, and I generally enjoy reading your thoughts and opinions. When I meet people I find interesting, I like to ask what they plan on doing with their lives. I understand completely if you don't want to share further details, but I for one would be interested in an off-topic detour into your intentions with these microsatellites. One application I always toy with in my head is a time+location verification service, but I don't think satellites are strictly necessary for that one unless you're trying to work around region-specific laws that would regulate towers.

K0SM0S 7y ago
Hi, I'm not sure if you'll get this late reply. First of all, thank you so much for your kind words, they mean the world to me, and for your interest — which is now reciprocal, I want to hear about you as well!.. I must admit I've spent way too much time trying to answer your questions in a 'concise' manner —HN's norm— but, as usual with this topic, it proved unusually hard fo me. It's rather complex, several independent yet synergistic 'moving parts' — too much repetition and cognitive bloat for a mere comment. Thus I'm drafting something to share and discuss the concepts, if time permits it'll be up on some website (maybe reddit, maybe a forum, maybe some blog, idk...) by month's end. I'll keep you updated, if you so wish. You can reach me by email `cosmos// a t //vcx.cx` ;-) The gist of it, FYI: - the satellite thing is a personal research project (in very tangible ways, the experiment is to actually do it and launch). But the endgame (think 2030-2040) is a massive swarm of ~8 billion devices or more, if you catch my drift. - However, it's an extension to a ground network which essentially aims at being an alternative infrastructure to internet. Formally it's something along the lines of a distributed, decentralized ("peer-to-peer") mesh network, fully encrypted yadi yada. - This network is but an "optional" medium for my original idea (in ~2010) which was, in dumb terms, a communication network (which people would call 'social network' I guess, but it's not against such existing services, it's more of a global standard / spec whose primary goals are security/freedom/privacy, interoperability (like email), and to be 'unstoppable' (in the event of war, catastrophe, etc). Going back to first principles, this 'network' is not even an application but a formal protocol I suppose. It's the kind of thing that would ideally exist as an RFC 'standard' by the IETF. This is more generally motivated by some of my philosophical values, notably freedom, empowering individuals (in the name of progress, civilization, but also happiness, self-growth).

pron 7y ago

> but your final paragraph seems to imply the formalism isn't key to end quality? That's not what I said. I said that merely creating a verified formal specification of a language is not in itself a good path to increasing correctness, and I wouldn't focus on that as a significant cause for concern given all others. But even when you use formal methods in the development of your software -- and I'm certainly a proponent -- there are many formal methods with widely different guarantees and costs, and some of them don't require a formal specification of the programming language. Moreover, no system can be 100% error free, regardless of verification method used. Systems rely on hardware whose actual behavior can never be "proven" correct, and, at best, only probabilistically matches the spec. I personally believe that some formal methods can greatly improve correctness, and do so affordably, but the question of which formal methods are worthwhile when and by how much each of them improves correctness is very much an open question. > it's the only working implementation of the concept of perfectly secured data. I strongly disagree. There is no such thing as "perfectly secure." Security is defined with respect to certain threats (e.g. a hazmat suit can protect you from poisonous gas but gives you no defense from bullets, whereas a bullet-proof vest is the opposite), and blockchain is rarely the most secure with respect to the most relevant threats in a monetary system.

AlphaWeaver 7y ago
> Security is defined with respect to certain threats, and blockchain is rarely the most secure with respect to the threats in a monetary system. Wow, this is a great way to frame this! What do you see as the largest threats to the effective operation of a monetary system?
- pron 7y ago
  I think this question is best answered by economists, and I'm certainly not one. But blockchain does seem to interfere with some of the best regulatory defenses against economic disasters.
  - rossdavidh 7y ago
    Blockchain gives the impression that the primary threat it is designed to defend against, is a government deciding (like Germany between world wars) to inflate their currency for whatever reason. So, not surprisingly, in order to defend a currency against being decreased in value by a central authority, it is vulnerable to all of the threats that a central monetary authority might help you with. Which of these threats you think is the more salient is, of course, a matter on which people may disagree. I personally find the risk of a central monetary authority devaluing my money, to be not one of my top concerns, but I could understand why others might think differently (especially if they were in a different country, that used a different currency).

ukj 7y ago

Beware of bugs in the above code; I have only proved it correct, not tried it. --Donald Knuth On the one hand we have the management mantra: if you can't measure it you can't improve it. On the other hand we have Goodhart's law. And so 'correctness', 'safety', 'quality' (or absence thereof) are fluid concepts that can never be formalised precisely. Language/logic sucks, but it's all we've got.

pron 7y ago
> Language/logic sucks, but it's all we've got. Perhaps, but PLT is not the main discipline studying software correctness -- those would be formal methods and software engineering -- although it has some overlap with those disciplines. PLT is not the general name for all study of programs; it is the name for a particular perspective, and a particular component of that study.