[andrewcanis]

Although there are Ethernet transceivers on the AWS FPGAs (these are Xilinx UltraScale+ VU9P FPGAs) they are unused and not connected directly to the AWS network. Instead the FPGAs are connected over PCIe to a host server, which has a standard NIC. This required us to use DPDK to bypass the kernel and pass raw network traffic directly to/from the FPGA over PCIe.

We have been told by cloud providers that the FPGA cannot be directly connected due to network security concerns. Since there is no easy way to control how the arbitrary hardware programmed by users on the FPGA will interact with their network. Microsoft has been using FPGAs directly connected to their network (called a bump-in-the-wire architecture) for the FPGAs used in their datacenter (see Project Catapult for details). But these FPGAs are not programmable by Azure users yet.

[analognoise]

I wonder if you could bound the problem with formal verification so that a custom design could only expose a certain activity profile, or an embedded hardware kill switch that would eliminate access after some detectable malicious interaction (at the hardware level).

Would that even be possible, or does it boil down to the halting problem (how can you know a sequence of transactions is malicious)?

[exikyut]

I'm completely naive, but even so I'm tentatively confident saying yes, it's a halting problem thing.

My understanding of formal verification is a) that it doesn't eliminate bugs, it just reduces their probability by a percentage, and b) that it's academically very attractive (which is why HN is constantly hearing about it) but practically very expensive in terms of investment/return, in the sense that formal verification requires formal modeling and so forth in order to exist in the first place, and that requires actual design lockdown, and suddenly everything got Complicated™ :)

You could possibly get away with an FPGA-targeting compiler (low-relevance related conversation: https://news.ycombinator.com/item?id=17151024) set up in a stripped-down form, but you'd need to lock it down a bit tighter than https://www.corsix.org/content/malicious-luajit-bytecode (a bit old, but illustrative of a point), and then the question would be whether that would negate the performance benefit of the FPGA in the first place.

The thread I linked the comment from had some interesting info on FPGA vs GPU (eg, https://news.ycombinator.com/item?id=17150985)