From a run-time perspective, there are lots of instances where untrusted code has to be executed and there are various sandboxing related approaches there (running in a walled off-VM for instance). From a deployment standpoint that doesn't scale if you need to have an actual VMware instance running per package/dependency. My hope is that a language implemented over a virtual machine might be able to achieve similar levels of security with less overhead.

Background: Open-source code has been an amazing boon for software productivity. However, I believe that most of the code that companies run isn't written by their own developers, it is from various packages and frameworks written by outside individuals and groups. My main focus is writing data intensive software where malicious actors, or just poorly written code, could compromise the confidentiality and/or integrity of customer data via a popular package/dependency. Better sandboxing of relatively untrusted code could be a huge boon for applications that have lots of plugins (think Chrome of VS code).

A few thoughts I have had on this front is limiting access of untrusted code to system calls that control file and network access is critical. Also, there would be a need to ensure that dependencies can't "takeover" a process by overwriting the call-stack to run their own code or spawning a new thread / process. Interested in your thoughts.

Comments URL: https://news.ycombinator.com/item?id=28988755

Points: 2

# Comments: 8

You mention in the description about testing code for all possible inputs. Are you all actually doing this behind the scenes with an SMT solver? Are you using some other proof assistant (COQ, HOL, etc) to be able to use proof-by-induction techniques and thus manage the path explosion problem?

I tried out an example comparing two multiplication algorithms (see below) and the tool said it couldn't find any issues in about a minute. Curious whether it will scale to larger problem sizes.

// implementation 1 int mult(int x, int y) { return x*y; } // implementation 2 int slow_mult(int x, int y) { int result=0; if(x<0) { for(int i=x; i<0; i++) { result-=y; } } else { for(int i=0; i ]]>Thu, 09 Sep 2021 03:04:00 +0000https://news.ycombinator.com/item?id=28465750SebastianFishhttps://news.ycombinator.com/item?id=28465750https://news.ycombinator.com/item?id=28465750I think you are speaking to one of the core tensions in formal methods. The difference between a specification and an implementation can get blurry. Where formal methods get interesting is statically proving properties about the specification. Take a simple example of a sorting algorithm. The two most commonly proved properties of these algorithms are that they 1) return a permutation of the input list (no items removed or duplicated) and 2) that the output of the list follow some sort of ordering.

One way to look at things is to say the permutation and ordering property checkers are the specification and the actual sorting algorithm is the implementation.

To your point about the specifications being Turing complete, some tools will put restrictions on the specifications to make function termination highly likely. COQ for instance requires that recursive functions be "decreasing in their inputs" AKA that subsequent calls to the same function are passed fewer items or elements than the parent.

Last point. I think that even writing a specification down to the level that it could be implemented using formal methods might be the biggest game changer. Agile stories rarely come even close to covering all of the potential edge cases. If we had a process that required product owners to literally think through all possible failure modes (what systems of formal methods do) and write out how to handle them then the cost of writing specifications would go way up. Per economics, I think we would end-up with simpler specifications which might be its own benefit.