There is a long-standing understanding that executing files out of world-writable directories is a security vulnerability (TOCTOU). That is why directories such as /tmp are often mounted with options such as noexec and nosuid in Linux. See for example: https://stigviewer.com/stig/red_hat_enterprise_linux_6/2016-12-16/finding/V-57569
By default, at least on stock Ubuntu 18.04 after installing the koka v2.4.0 .deb package, if the user does not manually create a ~/.koka directory, the koka interactive compiler attempts to use /tmp/.koka as the build directory, thus attempting to execute a binary out of a world-writable directory.
A user attempting to run koka interactively for the first time with a /tmp mounted as noexec would see the following error:
While this indicates there is no TOCTOU vulnerability, it can lead to frustration and poor first impressions if someone does not understand the implications of noexec mounts. Creating the ~/.koka directory is all that is needed to avoid the error. However...
The creation of app-specific dot-directories in a user's directory is a common and widely accepted practice. Assuming koka_build_dir is not explicitly set, I would rather see the koka compiler create the ~/.koka directory if so needed and use that instead of attempting to use /tmp to build and execute interactive binaries.
There is a long-standing understanding that executing files out of world-writable directories is a security vulnerability (TOCTOU). That is why directories such as /tmp are often mounted with options such as noexec and nosuid in Linux. See for example: https://stigviewer.com/stig/red_hat_enterprise_linux_6/2016-12-16/finding/V-57569
By default, at least on stock Ubuntu 18.04 after installing the koka v2.4.0 .deb package, if the user does not manually create a ~/.koka directory, the koka interactive compiler attempts to use /tmp/.koka as the build directory, thus attempting to execute a binary out of a world-writable directory.
A user attempting to run koka interactively for the first time with a /tmp mounted as noexec would see the following error:
While this indicates there is no TOCTOU vulnerability, it can lead to frustration and poor first impressions if someone does not understand the implications of noexec mounts. Creating the ~/.koka directory is all that is needed to avoid the error. However...
The creation of app-specific dot-directories in a user's directory is a common and widely accepted practice. Assuming koka_build_dir is not explicitly set, I would rather see the koka compiler create the ~/.koka directory if so needed and use that instead of attempting to use /tmp to build and execute interactive binaries.