Probabilistic Verification and Reachability Analysis of Neural Networks via Semidefinite Programming