Implication of ArrayBuffer in js bindings

[NikolajBjorner]

@bakkot - we are trying to understand the implications of the dependency for the ArrayBuffer.

does it break security requirements of some browsers?
the js bindings work for me, but I hear they don't always work out of the box.
in case it is a show-stopper for using the js bindings in a seamless way, should we change z3 internals to avoid it? (my understanding is that it is because of the time threads used in the main thread, so then inside of z3 we would spawn threads and join in the affected calls based on a setting).

@rlisahuang

[bakkot]

does it break security requirements of some browsers?

That's not quite how I'd put it. Rather, shared memory (which is necessary for threads) allows high-precision timers, which in turn make it easy to use Spectre side-channel attacks to leak any in-process memory. In the original model of the web, it was possible to load multiple pages from different domains in the same process. In combination with the previous point this would mean you could read data across domains, which is supposed to be impossible.

So, browsers only allow you to have shared memory if you specifically opt out of the ability to have pages from different domains in the same process as your page. This is done by serving the COEP/COOP headers. If you do this, the security model is fine with shared memory. If you don't, you can't use shared memory at all.

the js bindings work for me, but I hear they don't always work out of the box.

They'll always work in node out of the box (that is, when running locally rather than on a webpage), because node doesn't have the concern about cross-origin memory. But if you're trying to use them on a webpage, you'll need these special headers to allow the use of shared memory.

I expect node is the main use case. Using z3 on a website is mostly useful for demos and such, not for real problems.

in case it is a show-stopper for using the js bindings in a seamless way, should we change z3 internals to avoid it?

Eh, I wouldn't worry about it personally, at least not if it's going to be very much work. The extra headers are a little annoying if you're developing a website, but as the readme mentions, you can work around it by including a single extra script on the page (which will inject the special headers using a service worker).

[NikolajBjorner]

I guess I didn't make the context clear: We want to deploy web pages where you can run z3 in the browser.
It is for educational use, not for heavy lifting.

The goal is to make it installation free, ideally not depend on a server or other factors that could result in bit-rot.

The security question is directed towards being compatible with policies that browsers use. I didn't intend to ask a tricky technical question, rather about if there is anything known to be aware of for browser interop (which I am fairly clueless about), sorry.

[NikolajBjorner]

@pelikhan, please comment on your input

[pelikhan]

@bakkot thanks for the pointer on coi, this is very useful. We'll get to this once we integrate z3wasm in the browser. We are currently trying to run it in node.js (see other thread).

[bakkot]

@pelikhan Can you link the other thread? I'd like to follow along.

[pelikhan]

it started at microsoft/z3guide#19 but i think we'll split the issue for clarity

[pelikhan]

gameplan is to run z3wasm on all snippets at build time (with some caching) to precompute solutions