• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
      • Io
      • Defttag
      • Sys-call
      • Save-exec
      • Quicklisp
      • Std/io
      • Oslib
      • Bridge
        • Json-encoding
        • Security
          • Command
          • In-main-thread
          • Message
          • Start
          • Bindings
          • Stop
          • Try-in-main-thread
        • Clex
        • Tshell
        • Unsound-eval
        • Hacker
        • ACL2s-interface
        • Startup-banner
        • Command-line
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Bridge

    Security

    Important warnings about network security and the ACL2 bridge.

    The ACL2 bridge allows clients to run arbitrary Lisp commands, including for instance syscall. Because of this,

    If a malicious person can connect to your bridge, then he can read or delete your files, run arbitrary programs as you, and so on.

    To reduce the chances of this happening, you should probably only run the bridge on a unix domain socket. These sockets appear to have good security properties. (Per my understanding: remote users on the internet cannot connect to them, and they even offer some protection from other users on your system through the normal Unix filesystem permissions.)

    The bridge can also be run on an ordinary TCP/IP socket, but this is very scary because remote clients can connect. If you decide to run it this very scary way, then you should be very scared:

    • The bridge has no authentication mechanism, and will allow anyone who can connect to it to run any command.
    • The bridge sends all messages in plain text, so an eavesdropper can probably see everything you send to the server and everything it sends back.

    So, before you even think about putting the bridge on a TCP/IP port, you should make sure that, e.g., you have firewalls in place or are using SSH tunnels or something.

    Disclaimer. I am no security expert. The advice above is probably not enough to protect you. Please do not use the ACL2 Bridge without consulting your local security expert and network administrator.