StarMalloc: A Formally Verified, Concurrent, Performant, and Security-Oriented Memory Allocator