ABSTRACT
The networking infrastructure is a critical infrastructure for military operations. This infrastructure, however, can be complex to operate, due to challenges spanning multiple layers, from congested, contested communication links, to multi-domain operations, to application-aware mission networking. In this update, we introduce recent advances in applying formal verification to design highly robust, adaptive military networking. Specifically, we first introduce (1) recent advances in achieving real-time verification of large-scale, dynamic networks, (2) the transformation of centralized verification to fully distributed verification, to achieve provably correct military networking forwarding, and (3) the extension of verification from single domains to multiple domains, to support settings such as multi-domain operations and coalition. We then apply the verification capabilities to (1) drive robust adaptation, and (2) realize “horizontal” and “vertical” composition of multiple, heterogenous control planes, to improve military network capabilities, including robustness and efficiency. We provide both general frameworks and specific performance results to provide a systematic, informed update.

BIOGRAPHY
Professor Patrick J Baker is currently the Head of Science for the Royal Air Force, Air Information Experimentation Division and is Principal Technical Consultant C4ISR for the UK Ministry of Defence – Defence Science and Technology Laboratory. Patrick until recently was the Scientific and Technical advisor to the United Kingdom, Land Environment Tactical Communications and Information Systems replacement programme – this is a 10 year £5 Billion pound Capability replacement programme. Patrick is also very active with Academia/Industry through the US/UK Distributed Analytics International Technology Alliance, where he is the Principal Technical Advisor – through this alliance he is currently co-authoring white papers in support of Software Defined Networking with a particular user case of Software Defined Coalitions with Yale University in the US and Imperial College in London. Patrick has a large cohort of directly mentored students from undergrad through to PhD – he is a formal PhD marker for Loughborough University in the UK – where, he holds a Visiting Professorship in Communications and Information systems. Patrick often lectures in communications systems and technologies across a wide breadth of Government, Academia and Industry. Patrick is often called upon to brief at the highest level – as an exemplar – early this year briefing General Terrance J O’Shaughnessy – USAF – Commander - United States Northern Command and North American Aerospace Defence Command on advances within Mesh Networking and applicability to military user cases. Patrick is also currently advising the Republic of Ireland Army on procurement of future Operational and Tactical Communications capability. Patrick has had an interesting career spanning over 36 Years, initially within the Royal Air Force where he served in a number of communications engineering roles including directly with NATO. On leaving the service he has gone on to work with Boeing Satellite systems in the US, The United Nations - Balkans, The United Kingdom Ministry of Defence, the UK Foreign and Commonwealth Office, Cisco Systems, Nortel Networks, Ericsson’s development centre in Sweden, Nokia’s development centre in Finland as examples . Patrick’s breadth of experience has enabled him to develop and deliver diverse solutions/capability from communications protocols/systems through to novel Bio-metric collection and transfer techniques. In 2011 he was awarded a Chief Scientific Advisor to the UK Prime Minister award for outstanding work in support of Counter Improvised Explosive Device - Information Management and exploitation.

Professor Y. Richard Yang is a member of the Computer Systems Lab at Yale, where he founded and leads the Laboratory of Networked Systems (LANS). His research spans areas including computer networks, mobile computing, wireless networking, and network security. He led the P4P project (2008), which is the foundation for the establishment of the IETF Application-Layer Traffic Optimization (ALTO) Working Group and related Internet standards. Systems based on ALTO have been deployed in large-scale, production networks such as Deutsche Telekom since 2016. He led one of the most comprehensive research studies of Internet traffic engineering (2004-2010), with adoption by ATT (domain backup 2007), Cisco (ISP multihoming, 2004), and Google (COPE, 2006). He led one of the first systematic analysis and design of network localization (2004-2006), establishing the systematic network localization theory. He is a core member of the team that designed and implemented the first massive MIMO system called Argos (2012). He is among the first to design systematic, high-level network programming languages (Maple in 2013 and Trident 2018). His research has received extensive citations and featured in mainstream media including Economist, Forbes, Guardian, Chronicle of Higher Education, Information Week, MIT Technology Review, Science Daily, USA Today, Washington Post, and Wired, among others. He has received many awards, including the ACM SIGMobile Test of Time Award, US NSF CAREER Award, the Google Faculty Research Award, the Facebook Network Systems Award.