Trusted Systems Start with Education: A Call for Collaboration from TCCoE
The Trusted Computing Center of Excellence™ (TCCoE™) invites collaboration from educators, researchers, and practitioners committed to advancing formal methods and trustworthy systems. As part of our national education and training initiative, we’re seeking partners to help shape curriculum, develop materials, and expand outreach. If you’re attending the HCSS Conference or co-located meetings next week in Annapolis, we’d welcome the opportunity to discuss how you might get involved.
The mission of the Trusted Computing Center of Excellence™ (TCCoE™) is to lower barriers to adoption and facilitate the principled development and deployment of trustworthy software-based systems. Thus, risk will be reduced, especially in areas vital to U.S. and allied national defense, intelligence, security, and critical infrastructure. Rigorous mathematical proof offers strong evidence of trustworthiness, so the TCCoE fosters adoption of formal methods, as well as other advanced techniques, plus components and systems developed or verified with them. A leading example is the open source seL4™ microkernel. TCCoE goals include maturation of such technologies, stabilization of their software distributions, and expanding/training the user/developer base to provide much needed capabilities for the Nation.
An organizational architecture has been laid out, following strategic and tactical plans, to achieve the mission, through membership and workforce development, supported by 3 principal pillars: a shared repository for artifacts, tools and other materials; education/training in the artifacts, tools and techniques; and open protocol/software/hardware platforms facilitating evaluation, adoption and extension of all these.
Training and Education are essential to mission accomplishment. To improve the trustworthiness of computing bases for widespread use will require a much larger pool of formal methods researchers and practitioners plus exposure and encouragement of many more developers and users to adopt their artifacts.
Training is focused upon accelerating and expanding the near-term deployment and utilization of formal methods and their artifacts. This involves showing and providing hands-on learning experiences for current and future professionals in the usage of: the repo and its contents; the techniques, processes, and code of seL4; “lightweight” formal verification processes (e.g. running existing proofs against downloaded code, and slightly updating existing proofs to run against modified code, rather than developing entirely new proofs); analysis and testing of alleged TCB stacks; available vetted [open] platforms; etc. Materials can take the form of pamphlets, online tutorials, textbooks, or social media-based lessons and podcasts. Minimally, the TCCoE will act as a clearinghouse for materials that prepare trainees to use processes and resources that can deliver systems with the strong evidence of trustworthiness that the TCCoE promotes. The TCCoE should be capable and willing to act as a SME regarding relevant training materials. This would involve a periodic effort to identify such materials, acquiring soft copy if applicable, negotiating licenses as needed, and maintaining these materials in the repo (or, if externally hosted by a provider, linked via the TCCoE website). TCCoE will also run classes: on-line, at key locations around the country, and at employer sites.
Education involves a longer-term strategic goal. Although there are several universities actively involved in formal methods research, and most colleges offer courses teaching the fundamentals on which such methods are based (e.g. logics), there do not appear to be any curricula designed specifically to prepare students for working with them. The community needs a curated collection of educational materials for various purposes at various levels, e.g. from a 1-3 class session module introducing formal methods as a potentially rewarding career option, encouraging junior high school students to study Science, Technology, Engineering and Mathematics (STEM) generally and geometry specifically (as an introduction to formal proofs), through undergraduate and continuing education classes for practitioners, to graduate classes preparing students to conduct research. Curricular plans for concentrations in formal methods, teaching materials, and lab exercises, should be available within the repo. Exercises should run on and demonstrate configuration and use of the platforms.
The TCCoE will provide direct and indirect (i.e. supporting other education providers) educational services and materials/products focused on initiating future users, developers, and researchers, into: capturing not only functional but also non-functional (e.g. security) requirements; trustworthy-by-design/construction development; formal verification; developing on verified OSes in a manner taking advantage of their properties; creating complementary components (e.g. device drivers, network stacks) for open platforms; etc. Education will start by showing the value, to various demographics, of this approach. This must begin at an early age: the only exposure most Americans get to formal proofs is in high school geometry class, which many students detest (or avoid even taking); so there must be a unit for geometry teachers, showing the application of the concept to software, with opportunities for rewarding careers; and even a very small unit, exposing algebra students to the idea, to encourage them to take the subsequent geometry class. For that age group, to encourage students to become involved learners, the TCCoE will partner with high school honors program professionals and existing STEM (or STEAM) programs, especially those involved with math-letes or the National MATHCOUNTS competition. Similarly, the TCCoE must invest time, effort, and funding in partnering with undergraduate and Masters level institutions to formulate a concentration and perhaps specific courses in these study areas, which may involve a multi-year accreditation process. PhD level offerings must include not only advanced education in logics but also some hands-on work with proof assistants (interactive theorem prover tools).
Supporting this will be TCCoE supplied materials, including online tutorials, social media-based lessons, and promotional podcasts, directly usable by TCCoE instructors and indirectly supporting the efforts of other organizations. Partner educational institutions, or at least faculty on sabbatical or consulting, will be creating most of these materials. TCCoE Education Committee chairman Prof. Yong Guan of Iowa State University has offered to assist in developing a set of modules to be integrated with existing college and graduate-level courses. One possible 4 course on-line professional certificate program proposed by TCCoE Director Prof. Levy would cover:
- Designing trustworthy embedded systems
- Formal proofs of code correctness
- Cybersecurity basics (hacking 101)
- Advanced topics in cyber defense (side channels, time variations, FPGA decoding, etc.)
Finally the TCCoE must encourage roll-out across other academic institutions, not sufficiently immersed in formal methods to create the curricula, but educating computer professionals. Most materials would be offered at no charge to non-profit educational institutions. Basic on-line classes would be offered free to the public. Other on-line and in-person classes would be offered for fees. The TCCoE would also act as a portal, directing interested parties to educational institutions with their own relevant course offerings.
We solicit your assistance with any of the above, especially writing a proposal to funding sources to support development of curricula, then actually developing those curricula. Please contact any of the TCCoE Education and Training Committee volunteers via email or approach us in Annapolis next week:
Yong Guan, Chair
Renato Levy
Stuart Card
Michael Joseph