coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[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: [Coq-Club] Safe to download and compile .v from evil source ?
Date: Sat, 1 Feb 2020 14:32:39 -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-f178.google.com
Ironport-phdr: 9a23:hEiGhhVd7Yf5bwYI7sIsXY/D1EHV8LGtZVwlr6E/grcLSJyIuqrYYxKHt8tkgFKBZ4jH8fUM07OQ7/m8HzBaqs/f6DhCKMUKC0Zez51O3kQJO42sMQXDNvnkbig3ToxpdWRO2DWFC3VTA9v0fFbIo3e/vnY4ExT7MhdpdKyuQtaBx8u42Pqv9JLNfg5GmCSyYa9oLBWxsA7dqtQajZFtJ6osxRbFuHRFd/pZyW91JF+fgwv36sOs8JJ+6ShdtO8t+sBaXanmY6g0SKFTASg7PWwy+MDlrwTIQxGV5nsbXGUWkx5IDBbA4RrnQJr/sTb0u/Rk1iWCMsL4Ub47WTK576d2UxDokzsINyQ48G7MlMN9ir9QrQ+7qBx+x47UZ5yVNOZ7c6jAc94WWXZNU8BMXCFHH4iybZYAD/AZMOlXr4fzqVgAowagCwawH+7g0CNEi2Xs0KEmz+gsEwfL1xEgEdIUt3TUqc34OrkTUeCwy6nI0TXDbvNL0jrj8ofIaAshoe2SUrJ2asra1E4iFwLDjlWMrozlIS2a1v4Ds2if6OphW/mii2Eiqw5rozivwt0ghZXOhoIQ013J8zhyzoUtJdCgVkJ3fdqpHIFTuiyaLYd6XN8uTmJytConyLALupi2dzUQxps93R7QcfmHfpCI4h39UOaRJi91hHd/d7K+gxa+6Eygyu/hWsWt3lZGsyhIn9rWunAC0BzT7ceHSv9j8Uu7xTmP0AXT5vlFIUAyi6XbN4YszqAsmpcXq0jOHS/7lF/ogKOKdUgo4PWk5ubkb7n+o5+TLY50igXwMqQ0ncy/BPw1MgkIX2iH/uS8yqPs/Vf3QLVOif03nLLUsJ/fJcsBp665BxVZ3Zok6xa6FzumysgXnWEbLFJZfxKKl5TmO1bXIPzhEfi/h0msnyxwyvDdPrzhB43NIWLZnLfge7Z98U9cxxApwdBR/ZIHQo0Gdfn0Qwr6sMHSJh4/KQ29hej9W/tn0YZLZWOKBbOZIev5uEWT+u8pOKHYZYkJvyjwMfYh4OHGgnowmFtbdq6si8hEIEukF+hrdh3KKUHnhc0MRD9T4lgOCdfygVjHagZ9Im6oVvtltD4+AYOiS4zEQ9L12e3T7GKABpRTI1t+JBWJGHbseZ+DXq5VOi2XK85l1DcDUOr4EtJz5VSVrAb/joFfAK/U9ykf78yx0dF046jXl0h3+2UrX4KS1GaCS2wylWQNFWc7

Suppose a super-intelligent malevolent AI hands me a collection of .v files and asks me to compile them.

Is there *any* mechanism built into coqc which could be used by this evil oracle to hack my computer? Examples: ability to run shell commands, ability to write to disk, ability to detect whether or not a file at an arbitrary path exists or is readable, etc.

I *assume* the answer is "no, coqc is safe to run on untrusted .v from Internet," but I've been burned by that before (other languages) so I thought I'd better ask.

If the answer is "no," has that been the case for a nice long time, or is it only recently "no?" (Trying to gauge likelihood of bugs)

Sorry if this question is answered elsewhere; I searched but wasn't sure how to phrase the query

-t

[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