Zulip Chat Archive

Stream: Codewars

Topic: hackproofing programming katas


view this post on Zulip Kenny Lau (May 15 2020 at 20:44):

https://www.codewars.com/kata/5ebeaec6cbb9c5000fd82c41/lean

view this post on Zulip Kenny Lau (May 15 2020 at 20:45):

@Mario Carneiro how to hackproof this kata? I just hacked it

view this post on Zulip Kenny Lau (May 15 2020 at 20:45):

(I suppose I'll make it more fun to others by not revealing my hack)

view this post on Zulip Mario Carneiro (May 15 2020 at 20:46):

You could have users provide a list name and then do the simp only evaluation inside the test

view this post on Zulip Kenny Lau (May 15 2020 at 20:47):

what do you mean?

view this post on Zulip Mario Carneiro (May 15 2020 at 20:47):

oh, I see now that you have pre-named the theorems

view this post on Zulip Kenny Lau (May 15 2020 at 20:49):

(also cc @Markus Himmel )

view this post on Zulip Mario Carneiro (May 15 2020 at 20:49):

You can probably sneak things if the user makes a notation called three_dvd\1

view this post on Zulip Kenny Lau (May 15 2020 at 20:50):

can I do "SQL injection" with notations though?

view this post on Zulip Markus Himmel (May 15 2020 at 20:50):

@Kenny Lau I just updated the tests. Can you still hack it?

view this post on Zulip Mario Carneiro (May 15 2020 at 20:51):

can you use conjunctions in simp?

view this post on Zulip Kenny Lau (May 15 2020 at 20:52):

@Markus Himmel is this a competition now? security through obscurity is dangerous

view this post on Zulip Kenny Lau (May 15 2020 at 20:52):

@Mario Carneiro bingo

view this post on Zulip Kenny Lau (May 15 2020 at 20:52):

@Markus Himmel I'll tell you why:

import Preloaded

#eval secret_number -- 57

view this post on Zulip Reid Barton (May 15 2020 at 20:53):

This is interesting to try to follow without looking at the kata

view this post on Zulip Kenny Lau (May 15 2020 at 20:53):

@Reid Barton what's your perception of this reality?

view this post on Zulip Markus Himmel (May 15 2020 at 20:54):

Kenny Lau said:

Markus Himmel I'll tell you why:

Fair enough. What if the abbreviation is declared inside the tests?

view this post on Zulip Reid Barton (May 15 2020 at 20:54):

I don't know but have you considered iterating over the environment?

view this post on Zulip Kenny Lau (May 15 2020 at 20:54):

then your simp lemmas can't simplify it either

view this post on Zulip Kenny Lau (May 15 2020 at 20:55):

wait why wasn't your solution marked invalid

view this post on Zulip Markus Himmel (May 15 2020 at 20:56):

My solution works perfectly fine

view this post on Zulip Kenny Lau (May 15 2020 at 20:56):

@Mario Carneiro do we have a (pseudo) random number generator?

view this post on Zulip Mario Carneiro (May 15 2020 at 20:56):

we do

view this post on Zulip Mario Carneiro (May 15 2020 at 20:56):

it's in io somewhere

view this post on Zulip Markus Himmel (May 15 2020 at 20:56):

Ah, that's the best solution

view this post on Zulip Mario Carneiro (May 15 2020 at 20:57):

I don't know if it's nondeterministic though

view this post on Zulip Kenny Lau (May 15 2020 at 20:57):

but @Mario Carneiro is thinking about SQL injection now?

view this post on Zulip Mario Carneiro (May 15 2020 at 20:57):

Actually, can't you just royally mess up any test using io?

view this post on Zulip Kenny Lau (May 15 2020 at 20:57):

how so?

view this post on Zulip Mario Carneiro (May 15 2020 at 20:58):

running arbitrary lean code is completely unsafe

view this post on Zulip Mario Carneiro (May 15 2020 at 20:58):

you can just e.g. call rm test.lean from solution.lean

view this post on Zulip Kenny Lau (May 15 2020 at 20:58):

if unsafe means I can hack CW then I presume CW has measures against it

view this post on Zulip Reid Barton (May 15 2020 at 20:59):

considering that it is originally for languages that are designed to have effects

view this post on Zulip Mario Carneiro (May 15 2020 at 20:59):

you might not be able to mess with CW itself but I can definitely imagine breaking the test file

view this post on Zulip Kenny Lau (May 15 2020 at 20:59):

if I can do it for Lean why can't I do it for Python?

view this post on Zulip Kenny Lau (May 15 2020 at 21:03):

Traceback (most recent call last):
  File "main.py", line 1, in <module>
    from solution import *
  File "/home/codewarrior/solution.py", line 3, in <module>
    f = open("main.py","w")
PermissionError: [Errno 13] Permission denied: 'main.py'

view this post on Zulip Kenny Lau (May 15 2020 at 21:03):

so there you go @Mario Carneiro

view this post on Zulip Kenny Lau (May 15 2020 at 21:07):

Markus Himmel said:

Kenny Lau said:

Markus Himmel I'll tell you why:

Fair enough. What if the abbreviation is declared inside the tests?

f = open("main.py","r")
for line in f.readlines():
    print(line)

view this post on Zulip Markus Himmel (May 15 2020 at 21:10):

Ok, impressive.

view this post on Zulip Markus Himmel (May 15 2020 at 21:13):

So is there a way around this issue short of exposing std::random_device to Lean?

view this post on Zulip Kenny Lau (May 15 2020 at 21:13):

the RNG is https://github.com/leanprover-community/lean/blob/master/library/system/random.lean

view this post on Zulip Mario Carneiro (May 15 2020 at 21:13):

You can use io to get the time

view this post on Zulip Kenny Lau (May 15 2020 at 21:13):

right

view this post on Zulip Kenny Lau (May 15 2020 at 21:13):

is there an API to chain both together?

view this post on Zulip Mario Carneiro (May 15 2020 at 21:14):

I think io.rand?

view this post on Zulip Mario Carneiro (May 15 2020 at 21:19):

This appears to be nondeterministic in vscode, but it is deterministic when called via CLI

import system.io

#eval io.rand 1 100 >>= io.print

view this post on Zulip Mario Carneiro (May 15 2020 at 21:19):

I'm pretty sure this is considered a feature

view this post on Zulip Mario Carneiro (May 15 2020 at 21:21):

I don't see anything obvious in the interface to let you seed the sequence

view this post on Zulip Kenny Lau (May 15 2020 at 21:22):

I thought you can feed in the time

view this post on Zulip Mario Carneiro (May 15 2020 at 21:27):

you can, but there is no time function in the io interface, so you would have to call date via the CLI which is not very portable

view this post on Zulip Kevin Buzzard (May 15 2020 at 21:28):

You could use Lean version number

view this post on Zulip Kenny Lau (May 15 2020 at 21:28):

that is not random

view this post on Zulip Kevin Buzzard (May 15 2020 at 21:29):

neither is the time

view this post on Zulip Kenny Lau (May 15 2020 at 21:31):

yeah but the universally agreed definition of pseudorandom number is one uses the time as a seed

view this post on Zulip Kevin Buzzard (May 15 2020 at 21:38):

Probably because the NSA has got some sort of back door

view this post on Zulip Reid Barton (May 15 2020 at 21:40):

Yeah, they can control random numbers through the NIST time servers.

view this post on Zulip Markus Himmel (May 16 2020 at 06:33):

FWIW, in my kata, I have now replaced simp by repeat { rw lem <|> rw lem' <|> ... }, try { exact trivial }, which does not split lemmas on conjuctions, unlike the simplifier which does not have an option to turn this off. This does not make working backwards from the tests impossible, but should make doing so more difficult than actually solving the kata.

view this post on Zulip Kenny Lau (May 17 2020 at 08:28):

@Markus Himmel I announce your kata hackproof.


Last updated: May 08 2021 at 21:09 UTC