"Secure Safe Ambients" (SSA) are a typed variant of
"Safe Ambients" [Levi Sangiorgi 2000] whose type system allows 
behavioral invariants of ambients to be expressed and verified. 
The most significant aspect of the type system is its ability to
capture _both_ explicit _and_ implicit process and
ambient behavior: process types account not only for immediate 
behavior, but also for the behavior of process _residuals_, that
is for every possible evolution of processes in a given context. Based
on that, the type system allows the detection of security attacks such
as "Trojan Horses" and other combinations of malicious agents. 
 
We study the type system of SSA, define algorithms for type checking
and type reconstruction, define powerful languages for expressing
security properties, and study a distributed version of SSA and its
type system. For the latter, we show that distributed type checking
ensures  security even in ill-typed contexts, and discuss its use as a
formal justification of the Java Virtual Machine security architecture