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.