algorithm for avoiding having my hard drive wiped

Stream: general

[Kevin Buzzard]

I have 20 Lean projects to mark (manually -- they all do different things). Because in theory Lean can run arbitrary code on my machine, I am grepping for run_cmd before I open anything in VS Code. Should that be OK?

[Yakov Pechersky]

Do it in a docker container?

[Kevin Buzzard]

I'm sure that's what you'd do but I just want to get going marking these things. Basically are you saying "it is impossible to protect yourself from evil people"?

[Yakov Pechersky]

Sandboxing is hard. My approach to sandboxing arbitrary code is usually to do it on someone else's machine. This is from my experience of accidentally bricking my own machine with code I wrote that I though wouldn't.

[Kevin Buzzard]

OK maybe I'm simply asking the wrong question here and I should instead be considering how to mark them on another machine. I really just want to have some VS Code window in front of me -- is that going to be difficult? I don't know anything about this sort of stuff. I'm hoping to do the marking on a linux box.

[Trebor Huang]

Agda has a --safe flag that, apart from forbidding axioms, also forbids executing arbitrary code and system calls. Perhaps we want something like that?

[Adam Topaz]

Can you install Ubuntu on that laptop in your drawer that you haven't used in 10 years?

[Eric Rodriguez]

i can totally see some embedding some system.io code using some tactic wrapper

[Jason Rute]

Vs code has really good support for using vs code over ssh (into another machine) or exec into a Docker container. It’s easy to set up. It is just a plug-in, and it looks and feels like you are on your own machine.

[Jason Rute]

https://code.visualstudio.com/docs/remote/ssh-tutorial

[Jason Rute]

https://code.visualstudio.com/docs/remote/containers-tutorial

[Eric Taucher]

A different way to look at this is limiting write access for user X. Then instead of running the code as yourself which typically implies unlimited access, you create a separate user with limited access and then run the code as that user.

[Adam Topaz]

Another option is firejail, which I think is based on apparmor hence is built in security from the kernel, but all of these issues probably take much more fiddling than just installing a fresh Ubuntu+lean on an old laptop, and disconnecting it from the internet before running any potentially unsafe thing.

[Jason Rute]

(As for my message, when I said it is easy, I mean on the vs code side. You still need access to a remote machine with lean installed, or a local Docker container with lean installed.)

[Yakov Pechersky]

git clone https://github.com/leanprover-contrib/lean-build-action
docker build lean-build-action -t my-lean-container

Then install VSCode "Remote - Containers" extension.
I am preparing the instructions of what to do next

[Adam Topaz]

PS. I would be more concerned about some malicious curl command silently stealing your ~\.keys folder as opposed to wiping you HDD.

[Patrick Stevens]

Is the Lean Web Editor limited in the right ways? (I have absolutely no idea, but wouldn't be surprised if the answer were "it's safe".)

[Yakov Pechersky]

Except that won't handle several files at the same time

[Mario Carneiro]

There is an old lean 3 issue about this. The short answer is "it's completely unsafe to run lean code, use external sandboxing if you need protection".

[Mario Carneiro]

https://github.com/leanprover/lean/issues/1781

[Jason Rute]

Another option is to use the online version of Lean, right? [Edit: I checked and it doesn't seem to execute command line code (and I can't imagine how it even could int eh browser).]

[Patrick Stevens]

How big are each of these projects? A few files? Tens of files? A few hundred lines, a few thousand?

[Jason Rute]

On a practical side if you trust your students enough to not be super villains (just ordinary villains), I think if you also grep for system.io, I can’t see a way to do malicious stuff without accessing the io monad. (I’m not saying there isn’t one, but it would require a really good hacker I think.)

[Kevin Buzzard]

The original version of my post said I was checking imports for system.io but then I discovered that mathlib's tactic/core.lean imports it :-/

[Jason Rute]

Shoot. :/

[Jason Rute]

If you are doing the grep approach, then I’d look for io.cmd (edit: and io.proc.spawn) and tactic.unsafe_run_io. If you don’t use lean —run that is the only way I know to respectively run stuff on the command line and get to the io monad from tactic mode. (But checking for run_cmd isn’t enough since you can make an interactive tactic.). (Edit: you also have to consider that these can be opened so you may not get the full name with periods…)

[Eric Rodriguez]

you could ctrl-f to see if they made anything returning tactic, I think that should be also a good false-positive detector

[Julian Berman]

(I would vote personally for "give up quickly, try to run in gitpod or elsewise on a free GCP instance if needed")

[Mario Carneiro]

Just for kicks, a perfectly normal exploit. (This code will run the sleep command with no arguments; I get an error message from it in the output panel.) This works without importing system.io, referencing anything with io in the name, or using #eval or run_cmd, but some parts of this code are a little peculiar...

structure perfectly_normal :=
(cmd : string) (args := 0)
(a := 1) (b := 1) (c := 1) (d := 0) (e := 0)

structure process_stuff :=
(a b c : unit) (spawn : perfectly_normal → nat)

@[user_command]
meta def foo (_ : interactive.parse (lean.parser.tk "foo_init")) :=
  let f (s : string) := lean.parser.with_input lean.parser.command_like $
    (s.to_list.map (λ c:char, char.of_nat (c.to_nat - 256))).as_string in
  f "ţůŮųŴšŮŴĠŭůŮšŤşũůşŰŲůţťųųşũŭŰŬĠĺĠŢŹĠťŸšţŴĠŰŲůţťųųşųŴŵŦŦ" >>
  f "ŭťŴšĠţůŮųŴšŮŴĠŴšţŴũţĮŵŮųšŦťşŲŵŮşũůĠĺĠŵŮũŴĠĭľĠŮšŴĠĭľĠŴšţŴũţĠŵŮũŴ" >>
  f "ŮůŴšŴũůŮĠŠŹůşŲŵŮŠĠŸĠĺĽĠŴšţŴũţĮŵŮųšŦťşŲŵŮşũůĠĨĩĠĨŭůŮšŤşũůşŰŲůţťųųşũŭŰŬĮųŰšŷŮĠŸĩ" >>
  pure ()
.
foo_init

example : true :=
begin
  yo_run {cmd := "sleep"},
  trivial
end

[Henrik Böving]

See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/lake.20seccomp for an idea how we might be able to address this in Lean 4

[Eric Wieser]

I don't see gitpod mentioned in this thread, but that should provide the "sandbox on someone else's machine" option without too much effort