Towards A Verified Complex Protocol Stack in a Production Kernel: Methodology and Demonstration