diff options
| -rw-r--r-- | directions/directions.bib | 98 | ||||
| -rw-r--r-- | directions/research_directions.pdf | bin | 1247537 -> 1252961 bytes | |||
| -rw-r--r-- | directions/research_directions.tex | 155 |
3 files changed, 197 insertions, 56 deletions
diff --git a/directions/directions.bib b/directions/directions.bib index c760503..95b5ebf 100644 --- a/directions/directions.bib +++ b/directions/directions.bib @@ -1,6 +1,7 @@ @article{saxena01, author = {Saxena, Nitesh and Ekberg, Jan-Erik and Kostiainen, Kari and Asokan, N.}, journal = {Proceedings of the 2006 IEEE Symposium on Security and Privacy (S\&P{\rq}06)}, + localfile = {resources/saxena01.pdf}, publisher = {IEEE}, title = {Secure Device Pairing based on a Visual Channel}, x-color = {#009966}, @@ -10,6 +11,7 @@ @article{he01, author = {He, Debiao and Kumar, Neeraj and Lee, Jong-Hyouk and Sherratt, R. Simon}, journal = {IEEE Transactions on Consumer Electronics}, + localfile = {resources/he01.pdf}, month = feb, number = {1}, pages = {30--37}, @@ -22,6 +24,7 @@ @article{loe01, author = {Loe, Edwin Lupito and Hsiao, Hsu-Chun and Kim, Tiffany Hyun-Jin and Lee, Shao-Chuan and Cheng, Shin-Ming}, + localfile = {resources/loe01.pdf}, title = {SandUSB: An Installation-Free Sandbox For USB Peripherals}, x-color = {#009966}, year = {2016} @@ -30,6 +33,7 @@ @article{bates01, author = {Tian, Dave (Jing) and Bates, Adam and Butler, Kevin}, journal = {ACSAC}, + localfile = {resources/bates01.pdf}, month = dec, title = {Defending Against Malicious USB Firmware with GoodUSB}, x-color = {#009966}, @@ -39,6 +43,7 @@ @article{kobsa01, author = {Kobsa, Alfred and Sonawalla, Rahim and Tsudik, Gene and Uzun, Ersin and Wang, Yang}, journal = {Symposium on Usable Privacy and Security (SOUPS)}, + localfile = {resources/kobsa01.pdf}, month = jul, title = {Serial Hook-ups: A Comparative Usability Study of Secure Device Pairing Methods}, x-color = {#009966}, @@ -48,6 +53,7 @@ @article{kang01, author = {Kang, Myung and Saiedian, Hossein}, journal = {Information Security Journal "A Global Perspective"}, + localfile = {resources/kang01.pdf}, number = {4}, pages = {166--185}, publisher = {taylor\&francis}, @@ -59,6 +65,7 @@ @article{wang01, author = {Wang, Zhaohui and Johnson, Ryan and Stavrou, Angelos}, + localfile = {resources/wang01.pdf}, title = {Attestation \& Authentication for USB Communications}, x-color = {#009966}, year = {2012} @@ -67,6 +74,7 @@ @techreport{uzun01, author = {Uzun, Ersin and Karvonen, Kristiina and Asokan, N.}, institution = {Nokia Research Center}, + localfile = {resources/uzun01.pdf}, location = {Helsinki, Finland}, title = {Usability Analysis of Secure Pairing Methods}, x-color = {#009966}, @@ -76,6 +84,7 @@ @article{weinstein01, author = {Weinstein, David and Kovah, Xeno and Dyer, Scott}, institution = {The MITRE Corporation}, + localfile = {resources/weinstein01.pdf}, title = {SeRPEnT: Secure Remote Peripheral Encryption Tunnel}, x-color = {#009966}, year = {2012} @@ -84,6 +93,7 @@ @article{srivaths01, author = {Ravi, Srivaths and Raghunathan, Anand and Kocher, Paul and Hattangady, Sunil}, journal = {ACM Transactions on Embedded Computing Systems}, + localfile = {resources/srivaths01.pdf}, month = aug, number = {3}, pages = {461--491}, @@ -97,6 +107,7 @@ @article{arun01, author = {Kumar, Arun and Saxena, Nitesh and Tsudik, Gene and Uzun, Ersin}, institution = {Polytechnic Institute of New York Univesity \& University of California, Irvine}, + localfile = {resources/arun01.pdf}, title = {Caveat Emptor: A Comparative Study of Secure Device Pairing Methods}, x-color = {#009966}, year = {2009} @@ -104,6 +115,7 @@ @techreport{perrin01, author = {Perrin, Trevor}, + localfile = {resources/perrin01.pdf}, month = jul, number = {Rev. 34}, title = {The Noise Protocol Framework}, @@ -114,6 +126,7 @@ @article{angel01, author = {Angel, Sebastian and Wahby, Riad S. and Leners, Joshua B. and Blumberg, Andrew J.}, journal = {Proceedings of the 25th USENIX Security Symposium}, + localfile = {resources/angel01.pdf}, month = aug, pages = {397--414}, publisher = {USENIX Association}, @@ -126,6 +139,7 @@ author = {Su, Yang and Genkin, Daniel and Ranasinghe, Damith and Yarom, Yuval}, isbn = {978-1-931971-40-9}, journal = {Proceedings of the 26th USENIX Security Symposium}, + localfile = {resources/su01.pdf}, month = aug, pages = {1145--1161}, publisher = {USENIX Association}, @@ -138,6 +152,7 @@ author = {Tian, Dave and Scaife, Nolen and Bates, Adam and Butler, Kevin and Traynor, Patrick}, institution = {University of Florida}, journal = {USENIX Security}, + localfile = {resources/tian01.pdf}, location = {Austin, Texas}, month = aug, title = {Making USB Great Again with USBFILTER}, @@ -149,6 +164,7 @@ author = {Neugschwandtner, Matthias and Beitler, Anton and Kurmus, Anil}, institution = {IBM Research Zurich}, journal = {EUROSEC'16}, + localfile = {resources/neugschwandtner01.pdf}, location = {London, United Kingdom}, month = apr, publisher = {ACM}, @@ -168,6 +184,7 @@ @article{griscioli01, author = {Griscioli, Federico and Pizzonia, Maurizio and Sacchetti, Marco}, institution = {Roma Tre University}, + localfile = {resources/griscioli01.pdf}, publisher = {IEEE}, title = {USBCheckIn: Preventing BadUSB Attacks by Forcing Human-Device Interaction}, x-color = {#009966}, @@ -176,6 +193,7 @@ @misc{usb01, editor = {Dunstan, Bob and Ismail, Abdul and Wallick, Stephanie}, + localfile = {resources/usb01.pdf}, number = {Revision 1.0 with ECN and Errata through July 24, 2017}, publisher = {7 USB 3.0 Promoter Group}, title = {Universal Serial Bus Type-C Authentication Specification}, @@ -185,6 +203,7 @@ @article{kobeissi01, author = {Kobeissi, Nadim and Bhargavan, Karthikeyan}, + localfile = {resources/kobeissi1.pdf}, month = {dec}, title = {Noise Explorer: Fully Automated Modeling and Verification for Arbitrary Noise Protocols}, url = {https://eprint.iacr.org/2018/766.pdf}, @@ -196,6 +215,7 @@ author = {Krawczyk, H. and Bellare, M. and Canetti, R.}, month = {feb}, title = {RFC2104 - HMAC: Keyed-Hashing for Message Authentication}, + url = {https://tools.ietf.org/html/rfc2104}, x-color = {#009966}, year = {1997} } @@ -203,6 +223,7 @@ @proceedings{schiermeier01, author = {Schiermeier, Andreas}, journal = {26th Chaos Communication Congress}, + localfile = {resources/schiermeier01.pdf}, title = {TAN-Generatoren mit optischer Schnittstelle (Flickercode)}, url = {http://web.archive.org/web/20130309011417/http://www.hbci-zka.de/dokumente/spezifikation_deutsch/Belegungsrichtlinien%20TAN-Generator%20ve1.3%20final%20version.pdf}, x-color = {#009966}, @@ -225,3 +246,80 @@ year = {2012} } +@proceedings{tan01, + author = {Tan, Joshua and Bauer, Lujo and Bonneau, Joseph and Cranor, Lorrie Faith and Thomas, Jeremy and Ur, Blase}, + journal = {Proceedings of the 2017 CHI Conference on Human Factors in Computing Systems}, + localfile = {resources/tan01.pdf}, + location = {Denver, CO, USA}, + month = may, + publisher = {ACM}, + title = {Can Unicorns Help Users Compare Crypto Key Fingerprints?}, + x-color = {#009966}, + year = {2017} +} + +@inproceedings{chalkias01, + abstract = {Key establishment protocols are among the most important security mechanisms via which two or more parties can encrypt their communications over an insecure network. This paper is concerned with the vulnerability of one-pass two-party key establishment protocols to key-compromise impersonation (K-CI) attacks. The latter may occur once an adversary has obtained the long-term private key of an honest party, and represent a serious --- but often underestimated --- threat, because a successful impersonation attack may result in far greater harm than the reading of past and future conversations. Our aim is to describe two main classes of K-CI attacks that can be mounted against all of the best-known one-pass protocols, including MQV and HMQV. We show that one of the attacks described can be somewhat avoided (though not completely eliminated) through the combined use of digital signatures and time-stamps; however, there still remains a class of K-CI threats for which there is no obvious solution.}, + address = {Berlin, Heidelberg}, + author = {Chalkias, K. and Baldimtsi, F. and Hristu-Varsakelis, D. and Stephanides, G.}, + booktitle = {E-business and Telecommunications}, + editor = {Filipe, Joaquim and Obaidat, Mohammad S.}, + isbn = {978-3-540-88653-2}, + localfile = {resources/chalkias01.pdf}, + pages = {227--238}, + publisher = {Springer Berlin Heidelberg}, + title = {Two Types of Key-Compromise Impersonation Attacks against One-Pass Key Establishment Protocols}, + x-color = {#009966}, + year = {2009} +} + +@inproceedings{dechand01, + address = {Austin, TX}, + author = {Dechand, Sergej and Sch{\"u}rmann, Dominik and Busse, Karoline and Acar, Yasemin and Fahl, Sascha and Smith, Matthew}, + booktitle = {25th {USENIX} Security Symposium ({USENIX} Security 16)}, + isbn = {978-1-931971-32-4}, + localfile = {resources/dechand01.pdf}, + pages = {193--208}, + publisher = {{USENIX} Association}, + title = {An Empirical Study of Textual Key-Fingerprint Representations}, + url = {https://www.usenix.org/conference/usenixsecurity16/technical-sessions/presentation/dechand}, + x-color = {#009966}, + year = {2016} +} + +@techreport{rfc1654, + author = {Zimmermann, P. and Callas, J.}, + editor = {Johnston, A.}, + howpublished = {Internet Requests for Comments}, + institution = {{RFC Editor}}, + issn = {2070-1721}, + month = apr, + number = 6189, + pages = {1--115}, + publisher = {{RFC Editor}}, + title = {ZRTP: Media Path Key Agreement for Unicast Secure RTP}, + type = {{RFC}}, + url = {https://tools.ietf.org/html/rfc6189}, + x-color = {#009966}, + year = {2011} +} + +@misc{usbguard01, + author = {others}, + title = {USBGuard}, + url = {https://usbguard.github.io/}, + x-color = {#009966}, + year = {2019} +} + +@inproceedings{demaine01, + author = {Demaine, Erik D}, + booktitle = {International Symposium on Mathematical Foundations of Computer Science}, + localfile = {resources/demaine01.pdf}, + organization = {Springer}, + pages = {18--33}, + title = {Playing games with algorithms: Algorithmic combinatorial game theory}, + x-color = {#009966}, + year = {2001} +} + diff --git a/directions/research_directions.pdf b/directions/research_directions.pdf Binary files differindex 9a2b534..ff9610f 100644 --- a/directions/research_directions.pdf +++ b/directions/research_directions.pdf diff --git a/directions/research_directions.tex b/directions/research_directions.tex index 1e2ba2f..602d09b 100644 --- a/directions/research_directions.tex +++ b/directions/research_directions.tex @@ -535,12 +535,12 @@ to the attacker. \label{crypto_diagram} \end{figure} -To analyze the impact of disclosing the handshake hash to an adversary we must consider it's definition. The noise -protocol specification gives its definition, but does not % FIXME double-check this -guarantee that it can be disclosed to an adversary without compromising security. Figure \ref{crypto_diagram} contains a -flowchart of the derivation of both initiator-transmit and initiator-receive symmetric encryption keys $k_{1,2}$ and the -handshake hash $h$ during the Noise handshake. The definitions of MixHash and MixKey according to the Noise protocol -specification are as follows. +To analyze the impact of disclosing the handshake hash to an adversary we must consider its definition. The noise +protocol specification does not % FIXME double-check this +guarantee that the handshake hash can be disclosed to an adversary without compromising security. Figure +\ref{crypto_diagram} is a flowchart of the derivation of both initiator-transmit and initiator-receive symmetric +encryption keys $k_{1,2}$ and the handshake hash $h$ during the Noise handshake. Following are the definitions of +MixHash and MixKey according to the Noise protocol specification. \begin{align} \text{MixHash}(h,\text{input}) &= h' = H(h || \text{input})\\ @@ -548,7 +548,7 @@ specification are as follows. \end{align} Noise's hash-based key derivation function (HKDF) is defined using the HMAC defined in RFC2104\cite{rfc2104}. The hash -function $H$ employed here depends on the cipher spec used, in this work it is BLAKE2s. +function $H$ employed here depends on the cipher spec used. SecureHID uses BLAKE2s. \begin{equation} \text{HMAC}(K, \text{input}) = H\left(\left(K \oplus opad\right) || H\left(\left(K \oplus ipad\right) || \text{input} \right)\right) @@ -603,37 +603,6 @@ $h$. The channel binding method described above can be used in any scenario where a secure channel between two systems must be established where one party has a display of some sort and the other party has an input device of some sort. -\paragraph{Adaption to mice} Instead of a keyboard, a mouse can be used for pairing without compromising protocol -security. The host would encode the fingerprint bit string into a permutation -$\sigma(i) : \{n\in\mathbb N, n\le m\} \rightarrow \{n\in\mathbb N, n\le m\}$ -for an integer security parameter $m>0$ -and then display the sequence $\sigma(i)$ in a grid of buttons similar to a minesweeper field with an emualted mouse -cursor driven by pairing input on top. The user would then click the buttons on the grid in numeric order. The device -would do the same mouse emulation invisible to the user and would be able to observe the permutation this way. The -fingerprint can finally be checked by decoding the permutation into a bit string and comparing. The security level for -this method in bits is $\eta = \log_2(m!)$ or better than 80bit for $m=25$ in case of a 5x5 grid. See figure -\ref{mouse_mockup} for a mockup of what such a system might look like. - -\begin{figure}[h] - \centering - \includegraphics[width=7cm]{mouse_mockup.png} - \caption{A mockup of what mouse-based interactive pairing might look like} - \label{mouse_mockup} -\end{figure} - -\paragraph{Adaption to button input} -Adaption to button input using few buttons is a little bit harder. The obvious but impractical solution here is to have -the user enter a very long numeric string. Entering an 80-bit number on a two-button binary keyboard is not -user-friendly. One other option would be to emulate an on-screen keyboard similar to the ones used in arcade and console -video games for joystick input. This would be more user-friendly and would likely be a natural interface to many users -familiar with such games. One possible attack here is that if the host were to ignore dropped input packets, an attacker -might selectively drop packets in order to cause a desynchronization of host and device fingerprint input states. The -user would likely chalk up this behavior to sticky or otherwise unreliable keys and while they might find it -inconvenient, they might not actually abort the procedure. Thus it is imperative that the host verify there are no -dropped packets during pairing. This same observation is also true for keyboard or mouse-based pairing as explained -above, but an attack would be much more noticeable there to users as mice and keyboards are generally regarded reliable -by most users. - \paragraph{Relation to screen-to-photodiode interfaces} There have been many systems using a flashing graphic on a screen to transmit data to a receiver containing a photodiode held against the screen. Such systems have been used to distribute software over broadcast television but have also been @@ -670,6 +639,13 @@ transfer a key by simply reading out aloud the channel binding fingerprint. This out-of-band channel trusted for direct transfer of manipulation-sensitive key material to the problem of two users being sure whether they're actually talking to each other instead of an impostor. +A scenario using the SecureHID hardware to improve SSH security would be to terminate the SSH connection inside the +SecureHID hardware and this way prevent a compromised host from compromising the SSH remote. This approach has the +primary drawback that it would incur a large implementation overhead providing new attack surface. Additionally this +approach would only work when the user is solely interacting with the remote system through keyboard input and would +break workflows that require copying files to the remote host, or running commands in an automated fashion like a +configuration management system such as ansible would do. + \section{Hardware implementation} \subsection{Hardware overview} To demonstrate the practicality of this approach and to evaluate its usability in an everyday scenario, a hardware @@ -691,11 +667,13 @@ Additionally, those operations are only invoked infrequently any time the device % separate power supplies, possible future filtering of power/gnd and comms link signals \subsection{Usability considerations} + +\paragraph{Implementation robustness} In many systems such as common TLS-based systems, overall system security heavily depends on implementation details such as certificate checking and user interface details such as the precise structure of security warning messages and how they can be overridden. The complexity of these components in practice often leads to insecure systems, such as a system using TLS checking a certificate's internal validity but omitting checks on the certificate's chain of trust. A nice -property of the key estabilishment sytsem outlined in this paper is that it is both very simple, reducing surface for +property of the key estabilishment system outlined in this paper is that it is both very simple, reducing surface for errors and it tightly couples the critical channel binding step during key establishment to the overall system's user interface. In a system using either keyboard or mouse-based interactive channel binding, an implementation that does not perform the channel binding step correctly would simply not work. If the host does not display the correct fingerprint @@ -712,6 +690,71 @@ didn't the user would notice the device not functioning, but an attacker might h meantime. Likewise, the device needs a clearly understandable method of indicating pairing failure to the user. In practice a loud buzzer and a few bright LEDs would likely suffice for this. +\paragraph{Adaption to mice} Instead of a keyboard, a mouse can be used for pairing without compromising protocol +security. In a basic scheme, the host would encode the fingerprint bit string into a permutation +$\sigma(i) : \{n\in\mathbb N, n\le m\} \rightarrow \{n\in\mathbb N, n\le m\}$ +for an integer security parameter $m>0$ +and then display the sequence $\sigma(i)$ in a grid of buttons similar to a minesweeper field with an emualted mouse +cursor driven by pairing input on top. The user would then click the buttons on the grid in numeric order. The device +would do the same mouse emulation invisible to the user and would be able to observe the permutation this way. The +fingerprint can finally be checked by decoding the permutation into a bit string and comparing. The security level for +this method in bits is $\eta = \log_2(m!)$ or better than 80bit for $m=25$ in case of a 5x5 grid. See figure +\ref{mouse_mockup} for a mockup of what such a system might look like. + +\begin{figure}[h] + \centering + \includegraphics[width=7cm]{mouse_mockup.png} + \caption{A mockup of what mouse-based interactive pairing might look like} + \label{mouse_mockup} +\end{figure} + +\paragraph{Gamification} +A second, slightly more complex approach to a mouse-based interface would be to adapt the popular game Minesweeper to +compare fingerprints in our interactive setting. In Minesweeper, the user is presented with a fixed-size, say $20\times +20$ $x-y$ grid of fields. Under each of $n$ of the $x\times y$ fields a mine is hidden. The user is tasked with +uncovering all fields \emph{without} mines while \emph{flagging} those fields that contain mines. Every time the user +uncovers a field, the number of mines on adjacent fields is shown. If there are no mines on adjacent fields, all +adjacent fields are automatically uncovered by the game in a recusive fashion. The user wins when all mine-free fields +have been uncovered and all fields with mines flagged, and looses when they try to uncover a field with a mine on it. + +The fundamental approach to use minesweeper as a pairing method would be to encode the fingerprint into the minesweeper +field. The host would encode the fingerprint, then let the user play the game using their mouse with the usual on-screen +graphical representation of the game field. The device would besides forwarding all mouse input events to the host +simultaneously trace all user actions in order to Both host and device would emulate the game field and after a +successful run the user will have marked all locations of mines, thereby out-of-band transferring the field +configuration chosen by the host to the device. + +Minesweeper is very well-known and can be parametrized to be easily solved by most people. Compared to the task of +sequentially clicking buttons as presented in the previous paragraph a user might prefer playing a game of minesweeper +instead. While various problems surrounding minesweeper are computationally hard\cite{demaine01}, field generation is +easy. To place $n$ mines on a $x$ by $y$ grid one simply chooses an unordered subset of $n$ elements, of which there are +$\tbinom{xy}{n}$. For the three default difficulty levels provided by the minesweeper game included in Windows XP the +field state contains $\approx 40$, $\approx 156$ and $\approx 348$ bits of entropy respectively. This means even just +two rounds on beginner difficulty, or a single round on intermediate difficulty already provide a cryptographically +significant 80 bit security level. In the context of the interactive pairing protocol presented in this work, even a +single beginner-level round of minesweeper already reduces the chance of an undetected man in the middle attack to a +negligible level. + +A usability concern in this minesweeper-based pairing scheme would be user error. To improve user experience it would be +wise to still consider a round, even if the user makes a mistake and looses the game. A simple way to do this that also +intuitively handles user-set game difficulty levels would be to set a target entropy such as 40 bit, then repeat games +until the target entropy is reached with each game's outcome contributing to the entropy level depending on the +outcome's probability. +with a multivariate hypergeometric distribution here, jk + +\paragraph{Adaption to button input} +Adaption to button input using few buttons is a little bit harder. The obvious but impractical solution here is to have +the user enter a very long numeric string. Entering an 80-bit number on a two-button binary keyboard is not +user-friendly. One other option would be to emulate an on-screen keyboard similar to the ones used in arcade and console +video games for joystick input. This would be more user-friendly and would likely be a natural interface to many users +familiar with such games. One possible attack here is that if the host were to ignore dropped input packets, an attacker +might selectively drop packets in order to cause a desynchronization of host and device fingerprint input states. The +user would likely chalk up this behavior to sticky or otherwise unreliable keys and while they might find it +inconvenient, they might not actually abort the procedure. Thus it is imperative that the host verify there are no +dropped packets during pairing. This same observation is also true for keyboard or mouse-based pairing as explained +above, but an attack would be much more noticeable there to users as mice and keyboards are generally regarded reliable +by most users. + \section{Evaluation} % FIXME @@ -724,7 +767,7 @@ administration tool. Though we have done some basic security arguments in this p might be interresting for future use of this technology. We have soundly argued about the user experience benefits of our method, but we have not performed any field experiments to back up these arguments. Future research might analyze the practical security a system as outlined in this paper yields under real-world conditions. The various trade-offs of -e.g. keyboard vs. mouse input, fingerprint lenght and design details of the pairing UI might be analyzed with respect to +e.g. keyboard vs. mouse input, fingerprint length and design details of the pairing UI might be analyzed with respect to practical usability and security. \section{Conclusion} @@ -787,7 +830,7 @@ A working prototype has been completed. \item SRAM-based key storage with SRAM wear levelling \item host/device signature checking \item host/device key generation - \item proper circuit design because I was bored last weekend (see appendix \ref{ch:renderings}) + \item proper circuit design (see appendix \ref{ch:renderings}) \end{itemize} \subsection{Open issues} @@ -807,26 +850,26 @@ A working prototype has been completed. % \item Elaborate handshake security properties % \begin{itemize} % \item Possibly investigate other applications of this type of interactive handshake - \item Possibly contrast to carmera/other backchannel systems +% \item Possibly contrast to carmera/other backchannel systems % \item IMHO the pairing scheme is the most interesting part of this project from a scientific point of view % \item Prove security % \end{itemize} % \item Elaborate overall security properties of QubesOS-based system \item Elaborate possible DisplayPort/HDMI-based display encryption $\rightarrow$ Bunnie's NeTV2 w/ HDMI/eDP converter - \item Elaborate possible encrypted remote input (SSH) setups - \begin{itemize} - \item This might turn out to be really interesting - \item For this to be usable the host needs to tell the device at least which keyslot to use which could turn - out to be complex to implement securely - \item Considering complexity, this might turn into its own research project - \end{itemize} - \item Showcase secure hardware interface design, contrast with wireguard protocol design - \begin{itemize} - \item Formally derive handshake security properties - \item Formally derive host/device protocol security properties using noise spec - \item Formally verify and thouroughly unit-test the host/device protocol implementation on all layers - \item IMHO this is the most interesting part of this project from an engineering point of view - \end{itemize} +% \item Elaborate possible encrypted remote input (SSH) setups +% \begin{itemize} +% \item This might turn out to be really interesting +% \item For this to be usable the host needs to tell the device at least which keyslot to use which could turn +% out to be complex to implement securely +% \item Considering complexity, this might turn into its own research project +% \end{itemize} +% \item Showcase secure hardware interface design, contrast with wireguard protocol design +% \begin{itemize} +% \item Formally derive handshake security properties +% \item Formally derive host/device protocol security properties using noise spec +% \item Formally verify and thouroughly unit-test the host/device protocol implementation on all layers +% \item IMHO this is the most interesting part of this project from an engineering point of view +% \end{itemize} % Waiting \item Create custom hardware prototype \item Benchmark cryptography routines (will likely turn out to be ``wayyy fast'' for HID, fast enough for full-speed |