hackproofing programming katas

Stream: Codewars

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Mario Carneiro]

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

[Kenny Lau]

what do you mean?

[Mario Carneiro]

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

[Kenny Lau]

(also cc @Markus Himmel )

[Mario Carneiro]

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

[Kenny Lau]

can I do "SQL injection" with notations though?

[Markus Himmel]

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

[Mario Carneiro]

can you use conjunctions in simp?

[Kenny Lau]

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

[Kenny Lau]

@Mario Carneiro bingo

[Kenny Lau]

@Markus Himmel I'll tell you why:

import Preloaded

#eval secret_number -- 57

[Reid Barton]

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

[Kenny Lau]

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

[Markus Himmel]

Kenny Lau said:

Markus Himmel I'll tell you why:

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

[Reid Barton]

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

[Kenny Lau]

then your simp lemmas can't simplify it either

[Kenny Lau]

wait why wasn't your solution marked invalid

[Markus Himmel]

My solution works perfectly fine

[Kenny Lau]

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

[Mario Carneiro]

we do

[Mario Carneiro]

it's in io somewhere

[Markus Himmel]

Ah, that's the best solution

[Mario Carneiro]

I don't know if it's nondeterministic though

[Kenny Lau]

but @Mario Carneiro is thinking about SQL injection now?

[Mario Carneiro]

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

[Kenny Lau]

how so?

[Mario Carneiro]

running arbitrary lean code is completely unsafe

[Mario Carneiro]

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

[Kenny Lau]

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

[Reid Barton]

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

[Mario Carneiro]

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

[Kenny Lau]

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

[Kenny Lau]

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]

so there you go @Mario Carneiro

[Kenny Lau]

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)

[Markus Himmel]

Ok, impressive.

[Markus Himmel]

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

[Kenny Lau]

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

[Mario Carneiro]

You can use io to get the time

[Kenny Lau]

right

[Kenny Lau]

is there an API to chain both together?

[Mario Carneiro]

I think io.rand?

[Mario Carneiro]

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]

I'm pretty sure this is considered a feature

[Mario Carneiro]

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

[Kenny Lau]

I thought you can feed in the time

[Mario Carneiro]

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]

You could use Lean version number

[Kenny Lau]

that is not random

[Kevin Buzzard]

neither is the time

[Kenny Lau]

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

[Kevin Buzzard]

Probably because the NSA has got some sort of back door

[Reid Barton]

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

[Markus Himmel]

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]

@Markus Himmel I announce your kata hackproof.