Plan for external communication / isolation

[RalfJung]

Currently, the Miri interpreter only allows one kind of communication between the executed program and the outside world: printing to stdout/stderr. In the long run, that will not be enough. There were already requests for access to the system time, and it seems reasonable to ask for file system or network access. Getting proper randomness into the program might also be interesting.

This issue is basically the current status of #653, now that we [soon will] have a deterministically seeded RNG available in Miri all the time -- so much of the discussion there no longer applies.

It probably makes sense to allow external communication per default, just to get more programs running. But isolation is also a useful property, so I propose a -Zmiri-isolate flag to "turn off" external communication.

Assuming that's not very controversial, we have to decide what to do with the two existing systems we have in place that try hard to avoid allowing external communication:

• Environment variables. Should we just forward setting/getting env vars to the outside OS per default, and only keep using our current env var emulation layer when -Zmiri-isolate is set? That would resolve Support for accessing host environment variables #670.
• getrandom. Should we just ask the OS for "real" randomness per default, and only ask our internal RNG when -Zmiri-isolate is set?

Current status

• Add off-by-default "external communication" mode. Tentative name of the flag: ´-Zmiri-enable-communication.
• Allow interpreted program to access host env vars if external communication is enabled.
• Allow interpreted program to access host randomness if external communication is enabled.
• Come up with a less clumsy name for the flag that enables communication. Maybe -Zmiri-disable-isolation? Is that really less clumsy? -Zmiri-no-isolate?
• Turn external communication on by default?

[pvdrz]

I started working on the environment variables part of this issue. I added a new -Zmiri-enable-communication flag for this and I'm updating the get/set/unset env shims.

I am going to try to write the raw bytes of each env-var value and see what happens.

[RalfJung]

I'm updating the get/set/unset env shims.

I suggest introducing a new module, shims/env.rs, and moving all the env-related logic there.

[pvdrz]

Will do, I haven't decided what's the best way of handle allocations for the host environment variables. Currently I am creating temporary allocations for the variables and then deallocating them after writing.

Is it there any way to write some bytes directly into a PlaceTy instead of having to call write_scalar?

[oli-obk]

Can't you invoke the existing setenv logic?

[pvdrz]

What do you mean?

[RalfJung]

There's already code that does all the work of "given a C string, create an allocation for it". You should be able to re-use that. It's in the setenv shim.

The new thing here is that instead of doing this on setenv, it'll have to happen on getenv. So each getenv creates a new allocation that is then leaked. We should probably find a way to collect those, but for a first implementation that would be enough.

[pvdrz]

Oh ok yeah, That is what I am doing right now. I am deallocating each temporary allocation after using it.

[oli-obk]

Ah, I thought we'd just iterate over the env at startup and clone it into the miri env.

[pvdrz]

Well that might be easier and it would work unles someone decides to modify an env var while miri is running or something.

[RalfJung]

Ah, I thought we'd just iterate over the env at startup and clone it into the miri env.

Ah. That would fail to reflect later changes from "the outside" -- which is possible in principle. But I would be fine with this strategy as well.

[oli-obk]

Uh... I didn't know you could change env vars of a program while it was running

[RalfJung]

Hm, maybe you're not supposed to. But on Linux I suppose you could try to write to /proc/$PID/environ...

EDIT: nope, that file is read-only. I guess you are right.

[pvdrz]

Apparently you can do it using gdb, but that seems to be an unlikely scenario.

[RalfJung]

Agreed. Scanning the host env on initialization is fine. That's great as it makes the "communicate" and "dont communicate" cases much more similar: the only difference is that one starts with an empty env, the other with the real one.

[pvdrz]

Ok I will start working on this

Edit: In order to be able to allocate the env vars, we would need access to Memory and TyCtxt. Should I do this inside create_ecx instead of doing it inside Evaluator::new?

[RalfJung]

Status update: accessing host env vars is now possible with -Zmiri-enable-communication.

The name for that flag is preliminary, as is the fact that the current default for communication is off.

Also, IMO that flag should also make getrandom calls from the program use host randomness. Any objections to that?

[oli-obk]

Having a bunch of env vars given at startup feel very different to arbitrary communication at runtime, since everything is still deterministic given the same env vars

[RalfJung]

As far as I am concerned, the purpose of this "external communication" flag is to give up on determinism.

If we want to allow more things than "total isolation" while still being deterministic, I am open for that, but that's a gray area. For example, you could argue that allowing file access is also still deterministic if all accessed files are the same.

[pvdrz]

I think one could exploit something like the order of variables in #756 to do stuff in a non deterministic way.

Edit: nvm, if we are using the host's randomness this is not even a real concern

[oli-obk]

True. We can always add that back later if it seem desirable.

So..

Any objections to that?

Nope, bring on the cosmic rays

[RalfJung]

@christianpoveda do you want to try implementing that?

[pvdrz]

I'm working on it.

Edit: Now we are using the host's RNG when the communication flag is enabled

[RalfJung]

Closing this: we now have working external communication, and when/if we want to enable that by default, that should be a new discussion IMO. For now, off-by-default seems to still work fine.