Vulnerabilities

Stream: lean4 dev

[Henrik Böving]

Someone in power :tm: should probably respond to this: https://github.com/leanprover/lean4/issues/2189

[Sebastian Ullrich]

It can hardly be worse than "metaprogramming allows for execution of arbitrary IO values"

[Sebastian Ullrich]

Note that this "automatic vulnerability detection tool" (first red flag) raised identical issues in 800 other repos

[Eric Wieser]

I think it's probably still a good idea to turn on this reporting feature, even if we just ignore what's posted

[Henrik Böving]

Sebastian Ullrich said:

Note that this "automatic vulnerability detection tool" (first red flag) raised identical issues in 800 other repos

I gave them the benefit of doubt because their profile said PhD student :D

[Kevin Buzzard]

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

[Kevin Buzzard]

I marked all my student projects in a VM for this reason, even though "delete your lecturer's hard drive" is probably not an optimal approach for a good mark in my course.

[Johan Commelin]

How about "edit the lecturer's spreadsheet that records all the marks for the course"?

[Kevin Buzzard]

That would definitely be a good way.

[Sebastian Ullrich]

The issue and GitHub account have since been deleted, so that's that I suppose

[Mac Malone]

Sebastian Ullrich said:

The issue and GitHub account have since been deleted, so that's that I suppose

They have? I was still able to open the link to the issue (https://github.com/leanprover/lean4/issues/2189) -- which is still marked open -- and view their user account.

[Mario Carneiro]

I confirmed Sebastian's claim when he said it, as well as yours just now. It appears to have been a temporary existence failure

[Sebastian Ullrich]

Perhaps a temporary ban due to suspected spamming

[Notification Bot]

Eugene has marked this topic as resolved.

[Notification Bot]

Eugene has marked this topic as unresolved.