coder . cl

Standar ML is defined as safe using the following definition «ML is safe, in that a program that passes the type-checker cannot dump core, access private fields of abstract data types, mistake integers for pointers, or otherwise “go wrong.”». A type-checker verifies that each term used in the programming language should have the correct type once it is used. For example if a function is defined to receive an integer type, once it is called, an integer term should be used, otherwise the compiler may throw an error and the execution “goes wrong”. If the type-checking algorithm accepts the program, then it is well-typed. When a programming language has a type-checking algorithm on its compiler, we call it statically-typed. Dynamic typing does not have a type checker on its compiler, you can write the same function, it will not have any sentence defining an input type, and it will be able to receive a string when an integer is required.

Static typing have its basis on the “Semantic Soundness Theorem”. This theorem states that an environment p is on the domain of the type environment Γ, where each variable x in p respects the environment Γ. Then, if an expression e has the type τ in the environment Γ and the environment p respects Γ, the expression e in p has the type τ. In other words — if you have experience with Haskell or Standard ML — once you create a function of type τ, the function as expression should have the type τ. Seen from another perspective, if you define a function prototype in C as double f (double x), the type-checker will not allow another type than double.

There are two types of soundness, where we have weak and strong soundness. On weak soundness we can do some tasks like type casts, with strong soundness we cannot. On Java we can type cast returning values to another type, and the compiler will allow that. On other languages, like Haskell, type casting is implemented using its type system, but we cannot type cast variables using expression built in the compiler, because the type system uses strong soundness and does not have type casting operators, and each compile time error has a type, on Java each non related type — which is being type casted — does not have its own type. On strong soundness each variable and expression is strictly bound to a type within an error with the wrong type.

Java is not type-safe because it allows a very powerful way of organizing the type-space at run-time (through user-extensible class loaders ). This power can be utilized to write a program that exposes some flawed design decisions in the Java Virtual Machine. Specifically, one can produce a class A and an associated ersatz class A’ which can “spoof” A: its name N is the same as A, but it defines members (fields and methods) arbitrarily differently from A. A “bridge ” class B can be defined which delivers to a class D (for which the name N is associated with A’) an instance of A. D can then operate on this instance as if it is an instance of A’, thus violating type-safety. [Vijay Saraswat, “Java is not type-safe”].

We can have type safety implemented on the compiler using a type checker in compile-time, like Java does. Seems that it is not entirely safe on run-time, due to the research quote above. But seems that languages like Haskell are type-safe languages in compile-time too. But can you ask yourself what is the scope of type-checkers and its type-safety?. For me type-safety aims to be the correctness prover for each program. Like Agda and Haskell does, “a proof is a program; the formula it proves is a type for the program”. So, safety is not strictly bound to security, and it just defines the correctness of the program, not its environment.

I wanted to see how great Haskell’s static typing is, so I ran darcs under an LD_PRELOAD library that had a hacked open() call. [Zed Shaw, Twitter Quote].

Type safety just brings correctness, not security. Correctness provides security — in example a string cannot be used as integer — but not provides a full security layer, and we can define that type safety brings security in terms of correctness, and not its environment. Once a program is compiled, we cannot control its environment. With some very reduced set of examples, like Plesk. For example on not so early stage as web developer, I had a problem with Apache in the compiled version inside Plesk, giving me a core dump due to some Unicode characters on a configuration file, so I have tried to use the well known Linux strace(1), I have noticed that Plesk binaries were not allowed to run with the processor debug flags enabled. That is a way to control the environment, but I certainly cannot imagine a run-time enabled type-checker. What should be verified? Each variable?, Each function parameter?.

Although verification of type safety is not mandatory to run managed code, type safety plays a crucial role in assembly isolation and security enforcement. When code is type safe, the common language runtime can completely isolate assemblies from each other. This isolation helps ensure that assemblies cannot adversely affect each other and it increases application reliability. [Microsoft .NET Framework 4.5, “Type Safety and Security”].

I cannot expect that type-safety will bring me security. It only brings correctness in some manner, and the provided security only defined in terms of program correctness, rather than environmental. That is the common approach and I agree with it, we cannot expect that each program in our operating system keeps checking its environment and searching for flaws, that is a little bit weird and paranoid.