Let's assume the worst, that it's a VIP. Ok, now let's do some basic frequency statistics:
If you click the AS2650 link (1) in the article, you will learn that AS2650 is announcing 65,792 addresses in 5 prefixes. Roughly 40-70% of the IP addresses in a typical corporate ASN are associated with actual computers humans are using. Let's go with 40%. You're looking at 26,317 people. Assume they're all adults (please, dear lord, let them all be adults). 3-8% of the workforce is in IT. Let's go with 3%, that's 789 people. I'm guessing one of those 789 folks has thought this through and has a few VLANs set up to keep VIP and family-of-VIP, pattern of life stuff in a box.
As for the thesis that these are all window-licking low-IQ goons, that's just not how the US government cultivates its workforce. It's no accident that Harvard Business School characterizes themselves as "the West Point of capitalism." West Point isn't someone else's anything. The US Government is in it for the long haul and captures folks young with impossible-to-resist opportunities like the military academies, ROTC, SMART scholars, etc. Let's just stick with the academies: 12,000 people a year who were likely competitive for the Ivies, Division 1 athletics, or both, but chose their parents poorly. Free, top tier education and a job is very attractive for kids from fly-over states. Hell, in big states like California, New York, and Texas, it can actually be even more competitive. Something north of 60% of those graduates stick around for at least 20 years of service (because the high three pension + VA benefits is a pretty nice floor for retirement when your options back home are line supervisor at the cotton mill, the sugar mill, the coal mine, or ramp manager for United), usually addicted to the crazy level of mission. Sort of the opposite of finance where people really struggle mentally if they're not making pallets of money at an accelerating rate. Government service pays dogshit, but the work can super interesting, especially as you gain seniority.
Those folks then often loop back into other agencies and do another 20 years. Are there goombas in the Government? Oh, for sure. Absolutely. But it's roughly the same fraction as any other workforce in the rest of the economy.
But by the time you get to top tier stuff like the White House staff, the sorting function has been strong. To make the point: you also see top tier folks in other organizations with government stink on them. I can think of at least two directors at Google who are prior military. A fat pile of McKinsey folks. Something like 8% of Fortune 500 CEOs have served in the military, above the national average (6-7% of Americans have served in the military at some point).
And it's hilarious to watch people simultaneously assert the government is a bunch of idiots, and then get all excited about fighter pilots, the CIA, the CDC, ambassadors, the NIH. As though those people just appeared from the head of Zeus fully formed. Where do you think they worked when they were young? They were stamping visas for the Department of State in some embassy in central Asia. They were rolling blankets and digging wells in Gambia for the Peace Corps. Checking corporate filings for mostly unknown companies at SEC. Studying aerospace engineering at Embry Riddle and then flying cleared checks between clearing houses across the state overnight in a Cessna.
... and then Donald Trump as President, Stephen Miller as, whatever he is, and Peter Hegseth as Defense Secretary (he did serve in the military, if that's worth anything).
I think it's pretty wild to make all these bold assertions about the absolute top tier of elite talent that the US federal gov recruits and retains, and then compare/contrast that with the current staffers of the present incarnation of the executive branch. It just doesn't jive. Seriously, do a deep dive into Hegseth's resume and background of the nonprofit he was the figurehead for. He's more qualified than some known 3/4-star generals? Seriously? Tulsi Gabbard was the most qualified person for DNI? Seriously?
I agree that there's an element of kayfabe here. But it may be a case of "necessary, though nothing is sufficient": by making these noises, the community can at least know they've done this thing to alert other model providers of the concern. Can you acquire assurance that every model distributor will abide? No. But can you at least know that you've done what you can?
I mean, on the bio side, I've talked with the players and they know the concerns are real but at the same time very, very responsible members of the community have also said "But maybe the benefit really does outweigh the risk!?"
For those not in the know on governance, there are international organizations formed around treaties for similar situations, the IAEA and OPCW come to mind. I'm not aware of similar constructs for bio, cyber, or AI.
On the plus side, for these newer threats, you've got more than 30 minutes before the end of civilization. On the down side, the energy levels for the launch events are much lower, so much harder to detect.
Where does this leave formal verification? Are we just shit-out-of-luck at this point? You can formally verify everything about an airplane's code, but if any of that is wrong, ChatGPT might decide that the best way to help you win the Nobel Prize is to take down the airplane your chief rival for the prize is currently in.
I think formal verification has never looked better.
The main reason formal verification has never really taken off is that it's difficult.
LLMs are significantly more familiar with Lean and Rocq and TLA+ than most software engineers.
I think the cost of trying to build systems that adopt formal verification may have just dropped low enough that companies will consider them when previously the ROI didn't look like it was there.
I have had a lot of sympathy for this statement, LLMs could lower the bar to use of formal methods. But thinking it over in the context of BDD-driven development I am no longer really that sure. Compare two scenarios: A) from a specification an AI agent develops a usual piece of code along with a BDD-style testsuite passed and B) same AI also delivers a formal test (Lean/Rocq..) and successfully executes and passes it.
Will human judgment really consider scenario B) more credible than A) ? By so much that it is worth the effort ?
The first reason formal verification has never taken off is that it's difficult. The second reason, that most people don't get to because of the first reason, is that formal verification is really brittle. It is only verified under the very specific setup of the problem. Close doesn't count in math.
The first reason prevents humans from engaging with them, the second reason is what will make it difficult even for LLMs. I mean, I'm glad we are trying, but I'm dubious they will be the panacea some people proclaim.
Close can count in math - fuzzy logic and probability are a thing.
But I think you have it backwards. Close doesn't count in IT security. "Almost secure" means unsecure. Security is the compelling argument for formal verification.
If you click the AS2650 link (1) in the article, you will learn that AS2650 is announcing 65,792 addresses in 5 prefixes. Roughly 40-70% of the IP addresses in a typical corporate ASN are associated with actual computers humans are using. Let's go with 40%. You're looking at 26,317 people. Assume they're all adults (please, dear lord, let them all be adults). 3-8% of the workforce is in IT. Let's go with 3%, that's 789 people. I'm guessing one of those 789 folks has thought this through and has a few VLANs set up to keep VIP and family-of-VIP, pattern of life stuff in a box.
As for the thesis that these are all window-licking low-IQ goons, that's just not how the US government cultivates its workforce. It's no accident that Harvard Business School characterizes themselves as "the West Point of capitalism." West Point isn't someone else's anything. The US Government is in it for the long haul and captures folks young with impossible-to-resist opportunities like the military academies, ROTC, SMART scholars, etc. Let's just stick with the academies: 12,000 people a year who were likely competitive for the Ivies, Division 1 athletics, or both, but chose their parents poorly. Free, top tier education and a job is very attractive for kids from fly-over states. Hell, in big states like California, New York, and Texas, it can actually be even more competitive. Something north of 60% of those graduates stick around for at least 20 years of service (because the high three pension + VA benefits is a pretty nice floor for retirement when your options back home are line supervisor at the cotton mill, the sugar mill, the coal mine, or ramp manager for United), usually addicted to the crazy level of mission. Sort of the opposite of finance where people really struggle mentally if they're not making pallets of money at an accelerating rate. Government service pays dogshit, but the work can super interesting, especially as you gain seniority.
Those folks then often loop back into other agencies and do another 20 years. Are there goombas in the Government? Oh, for sure. Absolutely. But it's roughly the same fraction as any other workforce in the rest of the economy.
But by the time you get to top tier stuff like the White House staff, the sorting function has been strong. To make the point: you also see top tier folks in other organizations with government stink on them. I can think of at least two directors at Google who are prior military. A fat pile of McKinsey folks. Something like 8% of Fortune 500 CEOs have served in the military, above the national average (6-7% of Americans have served in the military at some point).
And it's hilarious to watch people simultaneously assert the government is a bunch of idiots, and then get all excited about fighter pilots, the CIA, the CDC, ambassadors, the NIH. As though those people just appeared from the head of Zeus fully formed. Where do you think they worked when they were young? They were stamping visas for the Department of State in some embassy in central Asia. They were rolling blankets and digging wells in Gambia for the Peace Corps. Checking corporate filings for mostly unknown companies at SEC. Studying aerospace engineering at Embry Riddle and then flying cleared checks between clearing houses across the state overnight in a Cessna.
(1) https://layer3intel.com/context/AS2650
reply