Software for rigorous optimization of real polynomials

I used QEPCAD once for this sort of problem, with reasonable success, although I think my problem was a bit smaller than yours.

First off, check out gloptipoly.

Also, there are general-purpose optimization packages which might work for you; they may be sufficiently fast to work even though they don't explicitly utilize the fact that the optimized function is a polynomial. Some of them require that you calculate the gradient, which in your case is easy. This a typical example; there are many such packages for R, say.

How complex are your polyhedra? Can you explicitly cover them with cubes, say? This may help you utilize those packages that only allow for simple lower and upper bounds on the variables. If you need a generic solution that may not be helpful, but if your polyhedron is fixed and relatively simple, this may be a workable approach.

I see Gloptipoly has already been mentioned. This is an implementation of the general sum-of-squares/Positivstellensatz methods which allow one to relax polynomial problems into convex optimization problems and in many cases produce certificates of optimality. Some related tools include SOSTOOLS and yalmip.

If you're interested in the theory you could search for papers by Parrilo, Lasserre, Nie, Putinar, etc. This paper by Peyrl and Parrilo in particular focuses on extracting exact (i.e. in terms of rational data) proofs of optimality, and I believe has an accompanying Macaulay2 package. Much of the general theory in this area is summarized well in the lecture notes for Parrilo's course at MIT OCW.

P.S. Can you tell from the post that Parrilo is one of my thesis advisors?