update ongoing research

Research/ongoing.html

@@ -32,21 +32,34 @@
       Heiser</a>
   </p>
   <p>
-    Trustworthy Systems (TS) is a research group in the School of Computer
-    Science and Engineering (CSE) at UNSW Sydney. TS works on building highly
-    secure operating systems for the real world. Their approach is based on
-    highly principled designs that support the use of rigorous formal methods to
-    ensure security and reliability without compromising performance.
+    The Trustworthy Systems (TS) group aims to make truly secure and safe
+    operating systems a reality. As a direct successor of the team that
+    originally created and verified seL4, it is focussed on principled and
+    verifiable seL4-based OS designs that achieve unprecedented security for
+    real-world systems without compromising performance.
   </p>
   <p>
-    Currently, TS&apos;s main activities are: Time protection, a principled,
-    fundamental approach for the systematic prevention of timing channels and
-    its implementation and verification in seL4; LionsOS, an seL4-based, fast,
-    secure and adaptable operating system for embedded and cyber-physical
-    systems; Pancake, a new low-level programming language designed to enable
-    the implementation and verification of low-level systems code, such as
-    device drivers; the design of a provably-secure seL4-based general-purpose
-    OS.
+    TS’s approach is to re-think and re-develop system architecture from
+    scratch, using fine-grained modularity, strict separation of concerns and
+    radical simplicity. TS also contributes to on-going development of seL4,
+    evaluating and improving kernel performance, and adding missing features
+    required by real-world systems.
+  </p>
+  <p>
+    TS’s current main activities are <a
+    href="https://trustworthy.systems/projects/timeprotection/">time
+    protection</a> – hardware and kernel mechanisms for principled prevention of
+    microarchitectural timing channels, <a
+    href="https://trustworthy.systems/projects/LionsOS">LionsOS</a>, a
+    statically architected, provably-secure, deployable OS for
+    embedded/cyberphysical systems, <a
+    href="https://trustworthy.systems/projects/pancake">Pancake</a>, a
+    verification-friendly systems programming language with a verified compiler
+    that is used for implementing and verifying LionsOS, and <a
+    href="https://trustworthy.systems/projects/Djawula">Djawula</a>, a
+    proof-of-concept of a general-purpose OS that can be proved to enforce a
+    fairly arbitrary security policy. TS open-sources all project code and
+    proofs.
   </p>
   '
   link="https://trustworthy.systems"