Software hacking
Contents
[hide]Proofs of non-hackability
Absolute certainty of absolute non-hackability one can never have.
Even if one has a formal proof that a software system can't be hacked,
the informal specification of properties that has been proven
could still be badly chosen i.e. incorrect or incomplete.
And if specification gets proven then there's a specification for the specification.
This leads to the Russel paradox, halting problem, and incompleteness theorem.
Esoteric, let's not go there.
Much more practically:
Formal proofs are still rarely done as (as of 2024).
We have no good tools for practically applying them yet.
Lack of such tools makes their practical usage extremely high in effort,
which is thus making them rarely applied.
Only in cases where really a lot is on the line. No matter the cost situations.
- There are good proof assistants (Coq & co) and
- there are many practical mainstream programming languages but
- there is nothing yet combining the two well enough yet. Not by a long shot.
What will eventually need to happen is a seamless integration of the
type level as a proof layer to the value layer (Keyphrases: "propositions as types", "Curry Howard Lambeck")
in next generation mainstream programming languages.
There are commendable attempts with dependently typed languages (Agda, Idris, …)
that give the type layer enough expressiveness to allow for proofs of properties on the value layer below.
But these languages lack features that make them suitable for mainstream usage.
- Libraries are lacking (especially in the graphics, UI, and browser area).
- Proofs can't be (easily or at all) gradually added later as partial programs (type errors == proof failing) do not run.
Novel type systems (like steady typing) capable of running partial programs (live)
will likely need structural editing, projectional editing, and micro-granular content addressed architectures.
Thus a paradigm shift away from code as lists of characters needs to happen eventually.
A good (proper) use of such a novel language would be applying
Conal Elliotts principle of denotative design to (DSL) libraries.
This also holds benefits in preventing bugs and improving on performance beside safety against hacking.
Illegitimate access via social engineering
Aspects to pursue:
- Education on common attacks
- Development of and education on novel means to check for authenticity (digital signatures - not just blockchain)
- Network of trust (voluntary! multidimensional! trust scores - avoiding social credit score ddystopia)
Various hacks - quasi random picks
There are very many variations. Listing even a fraction and discussing them would be a daunting task.
There are plenty of places on the web specializing on this. Please look at these to get an overview.
Here I'll only mention ones that for some reason or another seem particularly interesting.
Some scary ones actual tech experts fall for.
Ken Thomson Hack
The Ken Thomson hack is possibly the Nr1 most insidious one possible:
– https://wiki.c2.com/?TheKenThompsonHack)
"… a hack (in every sense), the most subversive ever perpetrated, nothing less than the root password of all evil. …"
"The source code for the compiler thereafter contains no evidence of either virus. "
"As the level of program gets lower, these bugs will be harder and harder to detect.
A well installed microcode bug will be almost impossible to detect."
" TheKenThompsonHack easily propagates into the binaries of all the inspectors,
debuggers, disassemblers, and dumpers a programmer would use to try to detect it. And defeats them.
Unless you're coding in binary, or you're using tools compiled before the KTH was installed,
you simply have no access to an uncompromised tool. "
– https://en.wikipedia.org/wiki/Ken_Thompson
– https://softwareengineering.stackexchange.com/questions/194746/what-is-the-ken-thompson-hack
Illegitimate access via session keys
- 2023 – Linus tech Tips – My Channel Was Deleted Last Night – https://www.youtube.com/watch?v=yGXaAWbzl5A
Hacking any phone
- 2024 – Vertiasium – Exposing The Flaw In Our Phone System – https://www.youtube.com/watch?v=wVyu7NB7W6Y
Cryptocurrency
Fake self-custody wallets on the web or even on supposedly safe app-stores when
slipping through the filters and not instantly recognized and taken down.
General
Very important is the concept of the attack surface.
– https://en.wikipedia.org/wiki/Attack_surface
Knowledge of friends and foes attack surfaces falls apart in the awareness–understanding matrix:
known-knowns, known-unknowns, unknown-knowns, and unknown-unknowns.
Making the attack surface absolutely minimal is risky too as one increases the risk of locking oneself out.
It's more like an optimizing balancing act.
Usage of cryptographic methods is very much a thing of "the right tool for the right job".
- The best encryption is also the slowest. One wants good ones and fast ones depending on the situations.
- Initial consensus on encryption keys can't practically use methods that'd require sending a secret physical letter.
Since there are a lot of jobs to get it right there are needed a lot of tools.
Thus the need to draw form existing libraries containing a huge amount of effort and expertiese
Ad hoc reinventing encryption strategies from scratch is naive and will most likely fail. AI?
AI will probably juts up the game for itself. We'll see.
