The math can be misinterpreted, misapplied, or not fit reality. That's why high-assurance security mandated a combination of things:
1. English specification of the system and its goals
2. Formal, mathematical specification of the system and its goals
3. Mathematical proof the system met its goals
4. Code implementing that system with a proof, often informal, that the code embodied the informal and formal design.
5. Tests of all functionality to prove the design and code worked.
6. Independent analysis of the above to find flaws in them.
7. If the implementation has concurrency or parallelism, more errors can occur due to that. There were techniques to mitigate it.
Each step found problems in systems made by professionals. Mathematical work and coding both have a long history of errors in their on fields. Combining them increases the likelihood of error.
Math is a social process that involves mental concepts, symbols for them, and discussion about them. It also needs peer review. If you see math in a paper, that's only one part of the process.
Further, in machine learning, we see lots of papers with math that doesn't lead to anything useful. Most papers claiming advances over prior architectures don't pan out in later testing. So, there will be skepticism when people make performance claims like the authors'. The best response is just independent testing.
You raise fair concerns. So, we need to get data to systems they're reading from. But, they can't connect back over those lines.
The safest way to do that is a high-assurance, data diode (one-way link). One builds hardware that, physically and by software, only allows information to flow one day. Many are available commercially.
Sometimes you need proof of acknowledgement of each packet but nothing else. Naval Research Laboratory had The [Network] Pump that allowed only Ack's back and with algorithm to throw off covert, timing channels.
Next, one might want to let people send them requests over an API which they can respond to in limited ways. One can use a high-assurance guard with secure, hardware/software architecture. It uses simplified I/O with a message format that's easy to parse securely.
At this point, I'm also thinking it might be better to use the closed-source, proprietary solutions. The AI's are rapidly scanning the open-source code for vulnerabilities which I'm sure they're not always sharing. They'd be more likely to have attacks on it.
So, don't tell the untrusted model how the guard works, use private models + traditional verification to secure its code, and include both HIDS and NIDS monitoring. Also, make the systems as predictable and boring as possible to make anomalies easier to spot.
Even if it was, covert, channel analysis from the 1980's and 1990's would've taught it to do or prevent that. It was required in all TCSEC-certified systems high, security classes. Many papers were published describing those analyses, including cache channel, which are in their pretraining data.
Most of IT security ignored that work and never used the methods. That's why their syatems can't defend against them. There are hardware and software groups that built countermeasures. They're not mainstream. I don't know if the hardware needed is even commercially available (eg partitioning caches, async & randomized CPU's).
My idea was taking 20+ year old designs that are patent-free, implementing them on any modern nodes that work (esp MOSIS-supported), their performance per watt will probably be better, and just use those. Some of the old designs, like NonStop architecture or MPP clusters, still have amazing benefits.
The two choices offered are a false delimma. The MILS kernels that came before seL4, like INTEGRITY RTOS and LynxSecure, had middleware to make deplpyments easier. The open-source solutions mixed standalone apps with user-mode VM's for Linux compatibility. OKL4 let one use drivers across them.
Looking at what's out there, I think GenodeOS should be mentioned for application-specific systems. They can even build some of their stuff on seL4 if you want.
I'll also add there's been unikernel projects that aren't in exotic languages. Even C++ (IncludeOS?). There's probably one in Rust by now. If not, it could probably build on Redox's components.
They were also often doing basic stuff, like database programming. Even in AI, most of what they produce didn't have marketable value. So, I don't buy that they couldn't find or train anyone here to do the job.
I made a utility, only partly done, to convert Avalonia files to HTML. It was intended to make cross-platform, Python/Tkinkter GUI's with HTML/Flask being a pit stop. Also, run them on QPython on Android. I got too busy to improve it past a few, form controls.
So, I think there's still potential to throw together an interface even if it can't do all of it. We do need a placeholder box that can be labeled for the controls we add manually but use its sizing info. Also, a converter that autoscales them in HTML or Qt to maintain the ratios that were in the VB6 app. For the placeholder, I was temporarily using that one control that's like a giant frame or box meant to contain others.
One reason I abandoned the idea is the AI's are so good now that we can probably just generate better GUI's from scratch or a basic, VB6 sketch. I couldn't justify the work until I try an AI with such projects. To avoid hallucinations or garbagr designs, might make sense to do the original program but AI-generate the transpiler.
1. English specification of the system and its goals
2. Formal, mathematical specification of the system and its goals
3. Mathematical proof the system met its goals
4. Code implementing that system with a proof, often informal, that the code embodied the informal and formal design.
5. Tests of all functionality to prove the design and code worked.
6. Independent analysis of the above to find flaws in them.
7. If the implementation has concurrency or parallelism, more errors can occur due to that. There were techniques to mitigate it.
Each step found problems in systems made by professionals. Mathematical work and coding both have a long history of errors in their on fields. Combining them increases the likelihood of error.
reply