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: Clément Pit-Claudel <cpitclaudel 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 18:18:01 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=cpitclaudel AT gmail.com; spf=Pass smtp.mailfrom=cpitclaudel AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk1-f176.google.com
Ironport-phdr: 9a23:tv8H3x/KKf9AZv9uRHKM819IXTAuvvDOBiVQ1KB20uIcTK2v8tzYMVDF4r011RmVBNmdt6kP07Se8/i5HzBZutDZ6DFKWacPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3wOgVvO+v6BJPZgdip2OCu4Z3TZBhDiCagbb9oIxi6sArcutMZjIZsJao91hrEqWZMd+hK2G9kP12ekwvy68uq4JJv7yFcsO89+sBdVqn3Y742RqFCAjQ8NGA16szrtR3dQgaK+3ARTGYYnAdWDgbc9B31UYv/vSX8tupmxSmVJtb2QqwuWTSj9KhkVhnlgzoaOjEj8WHXjstwjL9HoB+kuhdyzZLYbJ2TOfFjeK7WYNEUSndbXstJSiJPHI28YYsMAeQPM+lXoIvyqEcBoxalGQmhB/nixiNUinL436A31fkqHwHc3AwnGtIDqGrZrNHvM6cXT++1yrXIwi3ZYfNXxTfx8ZbFchQ7rvGRQL1/b87RwlQoGgzZllWQqJDlMC+R1usXrmiU8vRvVea0hm4orgF+uDmvxsM2hobVgYIVz0nJ+CNky4g7It24TVR0Yd+iEJZIrCGaK5F5Td8hQ252tyc11r0GtoS9fCgF1psr3QLQa/uCc4SQ4hPjU/uRIStlhH5/Y72wmRC/+lWjxO3kTsS4zkpGoy5fntTPtn0BzQLf5taZRvdn40us2zeC2xjN5uxFPUw4iK/WJ4Miz7M/k5cevlnPEyzqlEjzjaKbd1sr9+qt5unkeLrpu5qROo9phg3iN6kjnsyyDfk2PwULRGeW+Pqw26Pl8EbkWrtFlOc2nbPcsJ3CJcQUuKq5AwhN34Ym8Rm/DjOm3M0BnXkEMV5JYRyHg5XrNlzPOvz4AvC/g1OjkDdv2f/KJKHuApLILnTbkbfhe6hy61JExQYt0dxS44hYB7IBLf7pREP9qsLUAgUkPwG2wuvrENB92ZkfWWKLDK+ZKqTSsVqQ6+0zO+mMZZMVtyr5K/c/+v7hkGE2mVsGcKmm2JsYcnG4HvB8L0qFZnrsh88NEX0WsQomUOzqlFqCXCZPaHa1RqIw/y00CIa7DYjYXY2tm7yA3CKjHpJMfGxGC1aMEW3pd4qeQfsMZjiScYddlWkPUqHkQIs83zmvshX7wvxpNLn64Cod4LnnVd144fHkrRAusBdwBtmR3mXFG2psn38DQzYr0K17iUN4w1aHl6N/hqoLRpRo+/pVX1JiZtbnxOtgBoWqA1+TTpKyUF+jB+6eL3QxQ9Y2mYFcZk98H5C7jUmG0XP1XfkakLuEAJFy+aXZjSCoe5RNjk3e3axktGEIB9NVPDT/1KF6/gnXQYXOlhfBzvf4ReEnxCfIsVy74y+LtUBcXhR3VPycD38ab0rS69/+4xGbQg==

On 2020-02-01 17:53, Tej Chajed wrote:
> For some idea of some of the issues, see this thread on a similar
> question for compiling C:
> https://security.stackexchange.com/questions/138881/is-it-dangerous-to-compile-arbitrary-c.
> In particular see Matt G's answer, since he runs a site that compiles
> arbitrary C. Essentially he runs the whole thing in a VM that doesn't
> have secrets, and then has extra mitigations to give nicer error
> messages when people try to exploit the compiler.

Matt has a talk in which he mentions the security of Compiler Explorer where
he goes into a bit more details; see here: https://youtu.be/bSkpMdDe4g4?t=3193

Clément.

[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
        
        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 ?, Jason Gross, 02/02/2020
        
        Re: [Coq-Club] Safe to download and compile .v from evil source ?, jonikelee AT gmail.com, 02/02/2020