coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Safe to download and compile .v from evil source ?

From: Timothy Carstens <intoverflow AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Safe to download and compile .v from evil source ?
Date: Sat, 1 Feb 2020 14:51:46 -0800
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=intoverflow AT gmail.com; spf=Pass smtp.mailfrom=intoverflow AT gmail.com; spf=None smtp.helo=postmaster AT mail-lj1-f176.google.com
Ironport-phdr: 9a23:QD32NhU6W8FJ35MZTKwasket+2HV8LGtZVwlr6E/grcLSJyIuqrYYxGFt8tkgFKBZ4jH8fUM07OQ7/m8HzBbqdbZ6TZeKccKD0dEwewt3CUYSPafDkP6KPO4JwcbJ+9lEGFfwnegLEJOE9z/bVCB6le77DoVBwmtfVEtfre9FYHdldm42P6v8JPPfQpImCC9YbRvJxmqsAndrMYbjZZtJ6orxRbErGZDd+BKyW91P16ekAvw68mq8JJ/7yhcvu8q+tJdX6n9Y6k2V6FTAi48M2Ay6s3rtB3DQhWK63ABTGgYkQdGDhbc4h3iUZj/riX1tuxm2CmHJsL2Vqw7WS6j76hwVhDljjoMOiMj/2HWjsxwi79boA6kqhdizYPYfJ2ZOfxjda7bYNgUR3dOXtxJWiNODIOzbYsBAeQCM+hFsYfyu0ADogGiCQS2Hu7j1iNEi33w0KYn0+ohCwbG3Ak4EtwQsXTUqdL1NLsSUeG10aLF0y/Mb+lN2Tfh9ofIdAshquyLULJxd8rR1U4vFx3bgVWKp4zlOzSV1+oWvmiU6upvT+Ovi2o9pw5tpTivw94hh4/UjYwW0lDJ7Tt1zJoxKNGiS0N2YcSoHIVMuyyZLYd6X8EvTmButS0n0LMJo4S7czIPyJk/xx7QdfiHc4+Q7xLmTumRIDN4iGtheLK9mhq+6EagxvD+W8S1ylpKoS1Fkt7DtnAJyRPf8NSISvx4/ku52DaP0R7c6v1cLEwqiabWL4Qtz70wm5YJr0jPAiz7lF/rgKKUd0go4u2o5P7mYrXiqJ+cLYh0igTmP6QvnMy/HeM4MhYQUGiB9+S80Lrj/EPiTbVFi/05iKjZsJTAKcsHoa65BhdZ0pw/5BanEzemzNMYkGEbI1JCYRKLlpTmO1XTIP/jFvq/mFStkDJzx//cJLHhA5PNLmLCkLj7Z7p95VRcm0IPyoVU4IsRAbUcKtryXFXwvZrWFEwXKQuxltrmDdJh1pJWcmuVGbOUNria5V6O+uUxLvOCYIgKkDn4IvkhofXpiClqyhcmYaC10M5POziDFfN8LhDBOCe+spI6CW4P+zEGYqnqhVmFC2ABYn+zW+c45Gh+Btv5U8HMQYeihLHH1yC+TMUPNzJ2T2uUGHKtTL2qHvIFaSacOMhky2VWWr2oSotn3har5lajl+hXa9HM8yhdjqrNkcBv7rSKxx43/D1wSc+a1jPVQg==

Is anyone using this functionality for constructive purposes?

Does anyone have any tips on minimal path for getting there? I'd like to run a server that lets random Internet people upload .v for collaborative purposes. To facilitate collab, this server will need to typecheck those files. But if that's tantamount to letting them run Bash scripts, I'm gonna have a bad time.

I can setup all kinds of sandboxing and try to lock it down from the outside, but experience tells me this is a fool's errand (hard to document, maintain, test; just a lot of uncertainty in practice)

On Sat, Feb 1, 2020 at 2:41 PM Andres Erbsen <andreser AT mit.edu> wrote:

Redirect and Extraction commands write to the disk by spec. I reported it a while back and was told that I shouldn't expect coqc on unknown code to be safe in any sense.

[Coq-Club] Safe to download and compile .v from evil source ?, Timothy Carstens, 02/01/2020
- Re: [Coq-Club] Safe to download and compile .v from evil source ?, Jay Kruer, 02/01/2020
  - Re: [Coq-Club] Safe to download and compile .v from evil source ?, Andres Erbsen, 02/01/2020
    - Re: [Coq-Club] Safe to download and compile .v from evil source ?, Timothy Carstens, 02/01/2020
    - Re: [Coq-Club] Safe to download and compile .v from evil source ?, Tej Chajed, 02/01/2020
      - Re: [Coq-Club] Safe to download and compile .v from evil source ?, jonikelee AT gmail.com, 02/02/2020
      - Re: [Coq-Club] Safe to download and compile .v from evil source ?, Timothy Carstens, 02/02/2020
      - Re: [Coq-Club] Safe to download and compile .v from evil source ?, Clément Pit-Claudel, 02/02/2020
        
        Re: [Coq-Club] Safe to download and compile .v from evil source ?, Timothy Carstens, 02/02/2020
        
        Re: [Coq-Club] Safe to download and compile .v from evil source ?, jonikelee AT gmail.com, 02/02/2020
        
        Re: [Coq-Club] Safe to download and compile .v from evil source ?, Timothy Carstens, 02/02/2020
        Re: [Coq-Club] Safe to download and compile .v from evil source ?, Marco Servetto, 02/02/2020
        Re: [Coq-Club] Safe to download and compile .v from evil source ?, Jason Gross, 02/02/2020
        Re: [Coq-Club] Safe to download and compile .v from evil source ?, Timothy Carstens, 02/02/2020