You can call me Al, edition


Have I mentioned that KSE is an innovation in security engineering and design? It doesn’t work the same way as other things you’ve used before. For the newly curious, KSE is a COTS security sub-system that is easily loaded on to computer operating systems, augmenting their internal controls through a paradigm shift in trusted computing base design and implementation. Reference monitor capability to check user permissions, providing OS process separation, and kernel rule enforcement are just a few of the enhancements to the TCB delivered by KSE.

In the last post, “Where’s the Beef?”, I mentioned that this strong trusted computing enforcement that KSE provides is made possible through the use of the unique algebraic modelling that is its basis. This second part of this discussion on mathematical modeling will do a deeper dive into the real benefit that is derived, the fact that it delivers verifiable and consistent security.


Calls for more math use

Cryptography was the traditional domain f84ddacd8faf345f5d4d5ac64f42132bfor math use in infosec for a long time, but it’s used for spam filters, risk modelling, and more recently machine learning and data analytics. There is one area that used to be reserved for defence and intelligence sectors that is becoming more mainstream. Lately there have been a few more articles calling for greater embracing of math in the heart of systems, the kernel.

A few recent ones have discussed seL4 (Secure Microkernel Project), an open source Linux kernel which is already being looked at or used to protect drones, helicopters, medical devices and smart devices. One recent piece, “Unhackable kernel could keep all computers safe from cyberattack has as its bi-line, 

“From helicopters to medical devices and power stations, mathematical proof that software at the heart of an operating system is secure could keep hackers out”


The article discusses what should be commonly known by now, that weak OS and kernel security is the root of all infosec failure. It says this about seL4:

“Known as seL4, the kernel has a few highly secure properties: it can only do what it is designed to do; its code can’t be changed without permission; and its memory and data transfers can’t be read without permission.

two features underpin seL4’s security, one of which is a new way of isolating data inside the kernel. But the key development was making the code capable of being checked mathematically. Other kernels might have these properties too, but it is impossible to know for sure without mathematical proof, says Heiser.


The Devil is always in the details, doesn’t this seem like it would be a good thing? Most of the focus is on OS process separation, with seL4 being a microkernel (separation kernel), the purpose of such things being fault isolation by designing as much code as possible – from drivers to system services – to run in user space. If a fault happens in one part of the system, than you have guarantees that it can’t  propagate to other, possibly critical, parts of the system. This is a step forward in controlling access to the IT vulnerability surface, by reducing attack surface, but let’s be clear, security requires more than just fault isolation.

The folks promoting seL4 kindly point out that vendors of embedded devices, internet of things, drones and automobiles, and so on, need to embrace seL4 since their team claim to have proved mathematically that their kernel is unhackable.


Formal methods 

This type of mathematical proof is part of techniques known as formal methods used to show achievement of high assurance without impacting performance. From Wikipedia,

In computer science, specifically software engineering and hardware engineering, formal methods are a particular kind of mathematically based techniques for the specification, development and verification of software and hardware systems. The use of formal methods for software and hardware design is motivated by the expectation that, as in other engineering disciplines, performing appropriate mathematical analysis can contribute to the reliability and robustness of a design.

Formal methods are best described as the application of a fairly broad variety of theoretical computer science fundamentals, in particular logic calculi, formal languagesautomata theory, and program semantics, but also type systems and algebraic data types to problems in software and hardware specification and verification.

For any kind of certification indicating high assurance such as common criteria, especially for higher levels, the use of formal methods would certainly be a requirement. By the way, KSE also delivers separation kernel capabilities for OS process separation. KSE has been designed using “formal methods” for up to a common criteria certification of EAL 6, which is the highest possible for software. (EAL 7 possible with certain hardware.) Formal methods is of course used for its mathematical verification of assurance. Infosec needs a foundation of assurance, not assumptions based on herd consensus .


Why math counts

As it turns out, seL4 is not the only game in town in this respect. KSE is a mathematically verifiable, kernel-level security enforcer that provides fine-grained auditing and authorization control for every user’s operation on the operating system it is installed on.2a310c63c52e5bc43dd8dc4719f56052 Since I’m more familiar with it, I’ll use KSE as a reference for speaking of the advantages of algebraic modelling.

Defenders using KSE are assured that they are able to draw a hard line for a protection boundary, and it’s with the understanding that objects/processes behind that line will be protected. The basis for this view is not wishing or opinion, but algebraic analysis and mathematical proofs. This is something that enables Defender Advantage, but I’m not sure that this is understood well by everyone, or else things like seL4 would create more buzz. Perhaps some more explanation is in order.


Langsec impacts algorithms for security procedures

Awareness of Language-Theoretic, or Langsec, is growing. There are references to it in the definition of Formal Methods above, although they don’t use those terms. It informs us about design limitations of certain technical solutions in computer security. It often comes up in discussions of anything signature based, with AV being everybody’s poster child for this fail.

Computers are state machines and when running software programs, the state may remain unchanged until inputted commands in a program prompts transitions and changes of state to occur. An external state of a system can be composed of internal state machines. If you can break the internal states apart, the outside state is potentially no longer consistent if its nucleus has been impacted to attain some unintended state, or a “weird machine” by langsec lingo.

For example, we know that for Web applications, attacks can introduce either a new state or a hidden condition that generates a new sentential form inside a web app. Langsec informs us that this is something a regular expression language parser such as those commonly used in Web application firewalls, is going to find problematic. It is for this reason that current WAF construction incorporates a fundamental design flaw that violates some first principles of computing sciences  in regard to issues of decidability. Their regular expression make-up is dimensionally unable to completely detect the unintended states in software caused by attack code, (intentional or not).

Thus weird machines result from inconsistencies, and may occur when processes are not atomic, or unbreakable. Atomic operations are guaranteed to happen together.

Security procedures are just as susceptible to being lanced by langsec limitations. Say a security procedure has 5 steps. Is it possible to guarantee that none of those 5 steps can’t be broken? If something or someone, can disrupt or break any of the steps of your security procedure, then you have a problem.

When framed by a simple example of an algorithm the 5 steps of a chosen security procedure might be represented by something such as this to depict a process with stages and a supposed order of steps.

If A –> then B, If B –>then C,  If C –>then D,  If D –>then E

If any of the steps are not performed properly, they are broken/tampered with, or suffer an unintended consequence due to some unexpected input, then the final state may not represent what we think it does, or what is supposed to.

With algorithms, the steps are not verifiable. You don’t know if they have been done, or as intended throughout the procedure. You can say that you did step one, then step 2, and so on, but there is really no real way for myself or anyone else, to check that the individual steps took place, or that they executed in the way they were intended.


Al Gorithm meet Al Gebra

If one can modify that security procedure algorithm into an algebra, one can make it atomic and remove the opportunity to break it apart in the process. If there are negative connotations from use of the word unbreakable in infosec, it’s understandable. (Lesson: if you must label something in infosec as unbreakable, you probably should verify it mathematically!)

The great thing about an algebra is that if you do it successful, the end result is verifiable at the end. With algebra, as long as the equation being used has been solved correctly, one can check the answer by popping a result back in at the top to check its correctness. If an  equation is solved correctly, it can never be bent, or coloured. There is only just the correct answer; it’s like a fundamental truth and self-fulfilling prophecy simple-mathcombined. No matter how good a hacker is, he’ll never be able to change the fact that 2+2=4, and 4 is the answer. This is the major difference between algebra and an algorithm and because if this, an algebra can’t fail you in the way an algorithm might.

Algebraic operations are very cheap; one can do about a million of them per second. So you can also do millions in not much more time than the time needed to perform one, practically speaking. (They will always be faster than signature look-ups and are not dependent on a signature database being up to date.) And they can be very compact; they can be used just about on anything, even on embedded devices.


Pragmatic use

Verification is a pretty significant difference, and the major advantage of using algebra. Simple as that.  I think its fairly obvious which method might be a superior way to go. One shouldn’t have to be an Al Einstein to figure it out, at least on the surface. All one has to do is be able to frame all the security problems algebraically right? Or better yet, you can select a technology to use that does this already, like KSE. And by the way, KSE is not a microkernel, it’s a wrapper technology that you can drop it onto monolithic kernels and get the same benefit of this, and more, for use in embedded devices or all systems, just the same.

So what happens if the security primitives used by a technology are mathematical objects? They can’t be bent. They can be used to tailor rules used to control what needs to be controlled. They can be used to enforce rules. This plays out in the KSE reference monitor and plays out in that we have converted mandatory access controls and other security mechanisms into an algebra. It’s how KSE is able to run several trust models simultaneously on previously untrustworthy systems.

These common access control facilities allow security owners to create access rules using familiar and intuitive concepts. Since these facilities are implemented as security primitives, business rules don’t become opaque when implemented. This, in-turn, ensures that data in your systems and networks is contained within well understood boundaries of use, processing, distribution and access. It’s a means to align security with your business activities and goals. It is the verifiable security primitives which provide the foundation to build trusted execution environments on systems which in turn become the building blocks for verifiable chains of trust and trustworthy Defender Chains.


Mathematical completeness
Another important notion is that of mathematical completeness. With it, one can govern users and activities that may take place on a system with more fidelity, if so desired. (Consider an inside-in, outside-out environment.) This is  necessary for KSE to trust the part of the kernel it controls; there can’t be unknown variables. As one could imagine, this level of control is necessary for a trusted system. One of the reasons for poor metrics is it’s hard to measure a mitigation effort to reduce risk on systems that are not mathematically complete.


This is what KSE does, but there’s more yet to be explained, which I will do in the next post, as well as the ultimate; the algebraic model can be used to set up controls over access to the IT vulnerability surface, so that threats can’t exploit vulnerabilities, and one can protect vulnerable systems without patching.







Related sources

Is this Security-Focused Linux Kernel Really Unhackable?



< ——– Part 1: Where’s the beef? 

Part 3 For some hacker rejection, try math bijection ——– >