Last I looked you need a garbage collector to deallocate at which point you might as well use Java which is actually designed for that use case.

One of the points I am making is that when deploying on a modern multi-tenant VM-based platform, VM orchestration is analogous to process orchestration. However, you orchestrate the units, VMs, in a very different way to how you would orchestrate processes on say Linux. If your platform orchestrates, configures, and operates processes the same way a VM-based platform orchestrates, configures, and operates VMs and your implementation is solid then you would see similar security benefits. Virtualization is not the key. It just kind of looks that way because virtualization is usually paired with a fundamental re-architecture.

In greenfield application development or cases where you would do single-application VMs, you would target processes/platform directly. Only in situations where you are literally lifting code from a different OS environment that you can not or will not port to the native model would you need to go through a VM. If you orchestrate them the same way and your operational models for them are similar, then you will usually see similar outcomes. This is how it works in high security microkernels/separation kernels which simultaneously allow native processes alongside VMs. Virtualization is a feature to allow non-porting, it is not security/isolation; that is already provided underneath.

As independent evidence for this point, virtualization is not the basis of security/isolation in seL4. You have isolation without any virtual machines. Virtual machines are just a feature on top that can leverage the existing isolation functionality to also provide isolated virtual machines. Of course, a secure deployment then requires you to leverage this foundation with a good operational model and system design since you can always make a insecure system even atop a good foundation. This demonstrates that virtualization is not necessary for a secure base, nor sufficient to achieve highly secure systems.

Just to hammer in the point that you are heavily misinterpreting Theo's response, this is the full sentence at the start of the post that Theo was responding to:

"Virtualization seems to have a lot of security benefits. Rootkits can lie to DomU but not Dom0, and of course snapshotting, migration etc is really nice."

Wow, amazing, rootkits can never be in Dom0 because Xen has "virtualization" magic pixie dust. Theo is pointing out how this is nonsense and virtualization will only provide security if you can create implementations without glaring security holes. Furthermore, you should not just listen to the people who brought you insecure system 1 when they tell you that this time for sure they are going to give you secure system 2; maybe have just a little bit of cynicism and ask for some evidence first.

Since you are varying the security basis, implementation, and operational model simultaneously when you are comparing KVM to Linux to argue that the security basis is the important factor, I get to as well. Except mine is actually more fair because the design of a seL4-based system is actually much more similar to the design of a multi-tenant KVM-based system than the design of the KVM-based system is to the design of a Linux user environment.

Let us review a standard operational model:

Virtual machines are usually pre-allocated their total RAM. Virtual machines are usually pre-allocated a number of cores and pinned to them. Virtual machines are usually only allocated a small number of devices such as a virtual block storage device and virtual network device upon which they implement a in-VM filesystem and network stack. Virtual machines usually have no access to shared services provided by the hypervisor.

So we have a operational model where you have to pre-allocate RAM to a process. You have to pre-allocate a whole core and pin the process to it. The process has no access to a global filesystem, network stack, or devices. The process has access to exactly one file, which is logically similar to a virtual block storage device, and a single raw network socket, which is logically similar to a virtual network device. The process has no ability to form a socket to another process, form a new file, or even have any way of interacting with other processes at all. The process has no access to shared services of any kind.

The chasm between that operational model and any commercial IT operating system is immense, being basically the polar opposite in every dimension in the direction of security. Default-deny instead of default-allow. Shared-nothing instead of shared-everything. What you have there is a system even more static and simple than what runs on most microkernels. That is the comparable class of platforms with a similar operational model.

To demonstrate that virtualization is the key factor, you need to demonstrate that actually comparable systems with similar operational models like microkernels have more platform vulnerabilitys than comparable KVM-based, or even just hypervisor-based, systems. Which, again, flies against the face of evidence as the systems that are actually used in high security applications designed to protect against state actors are separation kernels instead of hypervisors.

It is the reduction to a smaller “kernel” that is responsible. If you applied the same design and operational model to running regular old processes instead of virtual machines you would also get a system with less security holes than the grossly insecure rat’s nest that is Linux, Windows, or whatever other commercial IT OS you have in mind.

Virtualization is almost entirely orthogonal, if not harmful, to security of the platform and operations. It is not magic pixie dust that makes your operational model more robust. You need a robust operational model, then you can have a robust operational model with virtual machines.

There is a reason why the most secure systems in the world are separation kernel architectures instead of hypervisors even though most of those systems do support virtualization as a feature, just not as the basis of their security propertys.

As the author and implementer of the algorithm allegedly prepared, ran, and analyzed benchmarks they obviously, by far, have the easiest time producing the evidence for their claim. Your argument that the poster needs to go read, implement, integrate, and benchmark the algorithm to to generate evidence to counter the absence of evidence for the claim is ridiculous. It would be as easy as 1-2-3 for the author to present their evidence to meet their burden of proof, yet you are demanding a extraordinary level of effort by the poster to present evidence against when they do not even have the burden of proof.

This is further ridiculous because the author or you would merely need to support the positive claim, where as you are demanding the poster demonstrate the negative, and all this before there is any evidence.

You should really stop with the unnecessarily combative tone when your entire model of argumentation is completely backwards in every respect.

I am confused how you got to “make the minimal thing that ticks of [sic] all of the must requirements”. I said engineering was about objective guarantees. Requirements are a derivative and means of that.

Making things better, more efficient, cheaper, etc. is not at odds with that. If you guarantee that level of performance and achieve it, then you have produced a acceptable instance meeting your guarantees. If you fail to meet your guarantees, then you have something unacceptable.

Despite the tolerances of a rocket-quality screw being far better than a car-quality screw being far better than a toy-quality screw, a car-quality screw does not get a pass in rockets because it is “better” than a toy-quality screw. It needs to meet the guarantees.

When you would rather have nothing over something that pretends to meet its guarantees, then you are probably in the vicinity of engineering.

This bridge is rated for 10 tons. This chemical process produces 1 mg 99% purity crystals. This biological process produces 90% pure insulin. This circuit handles 1 kA.

Engineering is not about better or worse it is about acceptable or unacceptable.

This naturally results in a desire for requirements so you can meet your guarantees. Specifications so you know what guarantees you need or what you are provided and how those map back to the real responsibility. Standards so you can consistently solve common problems.

You would be hard pressed to find a person who is more responsible or more representative of their organization than that.

Desalination, turning unlimited sea water into fresh water which is one of the most expensive sources of fresh water, is ~0.50 $/m^3. They can literally manufacture the water they use with zero impact on the water table for ~20 million dollars.

Capability passing is just extending that to the level of imports. Your files do not import the global I/O library and then use io.print(). They are passed a I/O library as the parameter {io} which defines a print() function and then call io.print().

That is permanently fixed and can be losslessly and perfectly converted to the corresponding date in the past if you care about what local time was at that instant at some location.

This argument is unfortunately empirically false for any program of any meaningful complexity (>1000 lines, probably even as low as >100 lines ignoring well-defined algorithms and data structures) using current formal methods.

Complete formal specifications are usually multiple times larger than the corresponding source code and encode esoteric propertys necessary for the proof, but which are largely even more impenetrable than a undocumented codebase.

So, it is both harder to figure out if you encoded the desired requirements and it is more complex. Your only advantage is confidence that what you wrote down is proven.

The thesis is that javascript-compatible source will be the substrate of the future. A javascript engine, though one highly optimized to efficiently interpret a compatible subset, is a potential universal platform of the future despite generic javascript being a terrible substrate.

WASM fundamentally rejects this by creating a new javascript-incompatible substrate that is actually designed to be a low level target. Claiming WASM is confirmation of the thesis makes as much sense as claiming that a future where everybody has a Rust interpreter in the browser is confirmation of the thesis.

If you are arguing that, then you are just arguing that web browsers will run code in some form in some language as they already do. As the video is clearly discussing a “surprising” possible future, it makes little sense for it to be consistent with literally business as usual and literally every possible future.

The government demonstrated that they are unqualified to keep data securely under their control. As such, any argument that a backdoor only allows the duly elected government access is empirically false. Any such backdoor empirically allows nefarious criminals access to your messages whereas the absence of a backdoor keeps your messages safely between you and the other party.

So, your options are:

1. Encryption with no backdoors so all messages are safe.

2. Criminals can freely read your messages so the government can more easily investigate potential criminals.

If you disagree, I presented the criteria for evidence needed to support your case. Remember, no shaky cam.

I imagine everybody relishes the opportunity to get smeared by entirely false accusations by Tesla promoters with a conflict of interest. You can tell the Tesla promoters running the smear campaigns are worth listening to because their smears keep getting disproved by video evidence.

Please point at any clearly visible video evidence that their whistleblowing is inaccurate. No "shaky cam" "Bigfoot" evidence where you point at something blurry and falsify a claim to fit your desired narrative.

Your job would have been a lot easier if any of those Tesla Promoters accepted the Dawn Project's offer to attempt the tests themselves with their own Tesla's and their own cameras giving them the perfect platform to debunk the Dawn Project's claims. Weird how they all chickened out on that slam dunk.