Typed assembly language

Typed assembly language incorporate typeness into assembly language .
It seems a viable approach to prevent security problem.

But it can only check program that contain source code. what if we download binary from internet?
There are some people doing researching on reasoning binary code.such as PCC(proof carrying code)

Can we incorporate type checking into CPU design?
Can we enforce seperation logic semantics by water print on pointer?