## Stream: Codewars

### Topic: hackproofing programming katas

#### Kenny Lau (May 15 2020 at 20:44):

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

#### Kenny Lau (May 15 2020 at 20:45):

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

#### Kenny Lau (May 15 2020 at 20:45):

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

#### 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

#### Kenny Lau (May 15 2020 at 20:47):

what do you mean?

#### Mario Carneiro (May 15 2020 at 20:47):

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

#### Kenny Lau (May 15 2020 at 20:49):

(also cc @Markus Himmel )

#### Mario Carneiro (May 15 2020 at 20:49):

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

#### Kenny Lau (May 15 2020 at 20:50):

can I do "SQL injection" with notations though?

#### Markus Himmel (May 15 2020 at 20:50):

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

#### Mario Carneiro (May 15 2020 at 20:51):

can you use conjunctions in simp?

#### Kenny Lau (May 15 2020 at 20:52):

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

#### Kenny Lau (May 15 2020 at 20:52):

@Mario Carneiro bingo

#### Kenny Lau (May 15 2020 at 20:52):

@Markus Himmel I'll tell you why:

import Preloaded

#eval secret_number -- 57


#### Reid Barton (May 15 2020 at 20:53):

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

#### Kenny Lau (May 15 2020 at 20:53):

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

#### 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?

#### Reid Barton (May 15 2020 at 20:54):

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

#### Kenny Lau (May 15 2020 at 20:54):

then your simp lemmas can't simplify it either

#### Kenny Lau (May 15 2020 at 20:55):

wait why wasn't your solution marked invalid

#### Markus Himmel (May 15 2020 at 20:56):

My solution works perfectly fine

#### Kenny Lau (May 15 2020 at 20:56):

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

we do

#### Mario Carneiro (May 15 2020 at 20:56):

it's in io somewhere

#### Markus Himmel (May 15 2020 at 20:56):

Ah, that's the best solution

#### Mario Carneiro (May 15 2020 at 20:57):

I don't know if it's nondeterministic though

#### Kenny Lau (May 15 2020 at 20:57):

but @Mario Carneiro is thinking about SQL injection now?

#### Mario Carneiro (May 15 2020 at 20:57):

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

how so?

#### Mario Carneiro (May 15 2020 at 20:58):

running arbitrary lean code is completely unsafe

#### Mario Carneiro (May 15 2020 at 20:58):

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

#### Kenny Lau (May 15 2020 at 20:58):

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

#### Reid Barton (May 15 2020 at 20:59):

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

#### 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

#### Kenny Lau (May 15 2020 at 20:59):

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

#### 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'


#### Kenny Lau (May 15 2020 at 21:03):

so there you go @Mario Carneiro

#### 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")
print(line)


Ok, impressive.

#### Markus Himmel (May 15 2020 at 21:13):

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

#### Mario Carneiro (May 15 2020 at 21:13):

You can use io to get the time

right

#### Kenny Lau (May 15 2020 at 21:13):

is there an API to chain both together?

#### Mario Carneiro (May 15 2020 at 21:14):

I think io.rand?

#### 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


#### Mario Carneiro (May 15 2020 at 21:19):

I'm pretty sure this is considered a feature

#### Mario Carneiro (May 15 2020 at 21:21):

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

#### Kenny Lau (May 15 2020 at 21:22):

I thought you can feed in the time

#### 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

#### Kevin Buzzard (May 15 2020 at 21:28):

You could use Lean version number

#### Kenny Lau (May 15 2020 at 21:28):

that is not random

#### Kevin Buzzard (May 15 2020 at 21:29):

neither is the time

#### 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

#### Kevin Buzzard (May 15 2020 at 21:38):

Probably because the NSA has got some sort of back door

#### Reid Barton (May 15 2020 at 21:40):

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

#### 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.

#### Kenny Lau (May 17 2020 at 08:28):

@Markus Himmel I announce your kata hackproof.

Last updated: May 08 2021 at 21:09 UTC