Long ago (1970s) our group at SDC was working on formal verification of our security kernels and - at least we tried - network security protocol.
(Our group included some early luminaries - Val Schore, Jan Garwick, John Scheid, Marv Schaeffer, Hillary Ormand - and later on Whit Diffie as a consultant.)
We had to design and code according to patterns and inject a kind of assertion language into the code. (Pascal language.) The verification was to try to see whether that conformed to "the criteria".
Turns out that coming up with the criteria against which to prove that the code conforms with the criteria is really, really hard, even for simple security models because one has to deal with things like low frequency data channels - like signalling (a potential security leak) by modulation of things like virtual memory paging or processor caches. We had to exclude channels < 300 bits/second, even knowing that that's a pretty wide channel.
Karl Auerbach
npub1rh…ps08d
2025-11-23 18:00:57 UTC
in reply to nevent1q…hgzk
Author Public Key
npub1rhqu8mlfa6tr2up0whlkr79xmkvrkwyzs6jj6u728ykxsqrnpneqxps08dSeen on
wss://relay.momostr.pinkPublished at
2025-11-23 18:00:57 UTCEvent JSON
{
"id": "3dc322d5c595aaed4c2c64de245ea8571797b0c9890e37bccdc80dea4c38aa7b",
"pubkey": "1dc1c3efe9ee9635702f75ff61f8a6dd983b388286a52d73ca392c6800730cf2",
"created_at": 1763920857,
"kind": 1,
"tags": [
[
"e",
"b425139cdf834a834191d80001b9a0f988c6389c2e9a9836ae5aa63b936c6ac2",
"",
"root",
"f1741fb3240636bce5f79baf275636768f08cb8b76deb7ed5f1e6feb63498eab"
],
[
"proxy",
"https://sfba.social/@karlauerbach/115600317301822062",
"web"
],
[
"p",
"f1741fb3240636bce5f79baf275636768f08cb8b76deb7ed5f1e6feb63498eab"
],
[
"proxy",
"https://sfba.social/users/karlauerbach/statuses/115600317301822062",
"activitypub"
],
[
"L",
"pink.momostr"
],
[
"l",
"pink.momostr.activitypub:https://sfba.social/users/karlauerbach/statuses/115600317301822062",
"pink.momostr"
],
[
"-"
]
],
"content": "Long ago (1970s) our group at SDC was working on formal verification of our security kernels and - at least we tried - network security protocol.\n\n(Our group included some early luminaries - Val Schore, Jan Garwick, John Scheid, Marv Schaeffer, Hillary Ormand - and later on Whit Diffie as a consultant.)\n\nWe had to design and code according to patterns and inject a kind of assertion language into the code. (Pascal language.) The verification was to try to see whether that conformed to \"the criteria\".\n\nTurns out that coming up with the criteria against which to prove that the code conforms with the criteria is really, really hard, even for simple security models because one has to deal with things like low frequency data channels - like signalling (a potential security leak) by modulation of things like virtual memory paging or processor caches. We had to exclude channels \u003c 300 bits/second, even knowing that that's a pretty wide channel.",
"sig": "0fc270d202a6abb1c67244550fcd8b45ad883a6315eb31e0cf1e9e5f69f62c3e28c023d5d55de458e8bc616ec94fce35f9826a75d7afa4608b6a60a45acf4715"
}