Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • From: Adam Chlipala <adamc AT csail.mit.edu>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Safe to download and compile .v from evil source ?
  • Date: Sun, 2 Feb 2020 09:51:46 -0500
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=adamc AT csail.mit.edu; spf=Pass smtp.mailfrom=adamc AT csail.mit.edu; spf=None smtp.helo=postmaster AT outgoing-stata.csail.mit.edu
  • Ironport-phdr: 9a23:GMx0ox2AqodA2b10smDT+DRfVm0co7zxezQtwd8Zse0RLvad9pjvdHbS+e9qxAeQG9mCt7QY1qGI7eigATVGvc/a9ihaMdRlbFwssY0uhQsuAcqIWwXQDcXBSGgEJvlET0Jv5HqhMEJYS47UblzWpWCuv3ZJQk2sfQV6Kf7oFYHMks+5y/69+4HJYwVPmTGxfa5+IA+5oAnMucQam4RvJ6Y+xhbIo3ZDZuBayX91KV6JkBvw+8m98IR//yhMvv4q6tJNX7j9c6kkV7JTES4oM3oy5M3ltBnDSRWA634BWWgIkRRGHhbI4gjiUpj+riX1uOx92DKHPcLtVrA7RS6i76ZwRxD2jioMKiM0/3vWisx0i6JbvQ6hqhliyIPafI2ZKPxzdb7bcNgHR2ROQ9xRWjRcDI2iYYsBD+kPM+hWoIbypVQBsRSwCBKwBO7s0DJEmmP60KM43uknDArI3BYgH9ULsHnMsNj6Kb0dUeWox6TWzTXDa/JW2S/n54jMaB8qvPaBUqhtfsXLzEkgCxjIgUmLqYP/PjOV0v4Bs22a7+p8T+6glXMoqxxorzWp28wiiZHJi5oIxlza9ih12og4KcGiREJle9KoDoZcuz2CO4doXs8vQ3tktDgmxrEbo5K3YSwHxI4pyhLBbfGMbpKG7Qj5VOmLJDd1nHJld6y7hxa16UWgzfD8VtW70FZNrypFlNbMumkW1xzP8MeHVuFy8l291jaUzQ/T6+VELVoxlaraN54t2KA/mYcOsUjbHy/2nlv5jLOOe0k55OSl6P7rb7v6qpOGKYN4kB/yPrkylsCnBOQ3KAkOX2yV+eSm073j+FX0T69XgfIsl6nWrIvXKtgApqGjAg9V1pwv6xO+Dze6ytgXg2QILE9ddBKdk4fpI03OIOz/Dfqnn1usly5ry+naMb3lH5XCNWPOkKzhfLZ4805T0hA/zdFZ55JOC7EOOuj/WkHrtI+QMhhsOAuthu3jFd9V14UEWGvJDLXKHrnVtAqh6usqa8KMYI4NsTL0Y6ws6/frhlcyglYcee+s3IdRZXylSKc1a36FaGbh149SWVwBuRAzGbSz2Q+yFAVLbnP3ZJoSozQyCYaoF4DGH93/i6eI3SP9G5xKIG1KFwLVSCu6R8C/Q/4JLRmqDIp5iDVdCOqqUIYg0VertRO8xrZ6fLKNp38o8Kn73d0w3NX90BE/8TsvV5aazn2CSGBykSYTWzYq1eZ0ukV8zhGG0LQ+jvBFR4Re

On 2/1/20 11:30 PM, Timothy Carstens wrote:
Consider the following workflow:[...]
5. User runs coqc foo.v

[...]

If so, then (5) is inherently an unsafe thing to do, and in that case I don't see how Coq could be used to certify untrusted code. You'd need to first do a code review of the ltac and everything else to convince yourself that it was safe to compile.

I think this might be a case of many people on this mailing list taking workflow details for granted and not realizing they should be spelled out.  No, the clear community recommendation would be to check .vo files, not .v files.  However, that mode requires additional code-review tools that pretty-print crucial parts of .vo files in sufficiently readable ways (definitely not involving Ltac, plugins, etc., and in fact with no need to display proof terms, just "final" theorem statements and their dependencies).

jonikelee AT gmail.com
wrote:

I once used an
antequated proof system (pvs) that had a tactic language but also had
the ability to "macro-expand" the tactics into atomic proof steps and
record the resulting fully expanded proofs in a file. Having that
eliminates the need to run the tactic language later to verify the
proof, and thus the possibility that someone can exploit the tactic
language.
That sure sounds like .vo files and, in general, the trust philosophy at the heart of the Coq project since the beginning.




Archive powered by MHonArc 2.6.18.

Top of Page