There's a lot of work in CompSci on this that predates all the blockchain-related stuff. They usually call it "security-typed languages" or "information flow security." Here's a paper with a lot of prior work in that plus an example tool and language:

https://www.cs.cornell.edu/andru/papers/jsac/sm-jsac03.pdf

https://www.cs.cornell.edu/Projects/fabric/

The concept was taken to the binary with Necula's Proof-Carrying Code. Work like Kumar's and Davis' eliminated most of the TCB of the provers, too.

https://www.utdallas.edu/~hamlen/Papers/necula97proofcarryin...

http://www.cse.chalmers.se/~myreen/runtimes.html

In parallel, there's always work in capability-based security applied to programs or OS's. Here's an old and new one using that model.

http://erights.org

https://www.ponylang.org